A. Aggarwal & J. S. Vitter (1988):
The input/output complexity of sorting and related problems.
Communications of the ACM 31(9),
pp. 1116–1127.
S. Allmaier, S. Dalibor & D. Kreische (1997):
Parallel Graph Generation Algorithms for Shared and Distributed Memory Machines.
In: G. Bilardi, A. G. Ferreira, R. Lüling & J. D. P. Rolim: Proceeding of the Parallel Computing Conference PARCO'97 (Bonn, Germany),
LNCS 1253.
Springer,
pp. 207–218.
Available at http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.17.2006&rep=rep1&type=pdf.
Tonglaga Bao & Michael Jones (2005):
Time-Efficient Model Checking with Magnetic Disk.
In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005),
LNCS 3440.
Springer,
pp. 526–540,
doi:10.1007/978-3-540-31980-1_34.
J. Barnat, P. Bauch, L. Brim & M. Češka (2010):
Employing Multiple CUDA Devices to Accelerate LTL Model Checking.
In: 16th International Conference on Parallel and Distributed Systems (ICPADS 2010).
IEEE Computer Society,
pp. 259–266,
doi:10.1109/ICPADS.2010.82.
J. Barnat, P. Bauch, L. Brim & M. Češka (2011):
Computing Strongly Connected Components in Parallel on CUDA.
In: International Parallel & Distributed Processing Symposium (IPDPS'11).
IEEE Computer Society,
pp. 541–552,
doi:10.1109/IPDPS.2011.59.
J. Barnat, L. Brim & I. Černá (2002):
Property driven distribution of Nested DFS.
In: Proc. Workshop on Verification and Computational Logic,
DSSE Technical Report DSSE-TR-2002-5.
University of Southampton, UK,
pp. 1–10.
Available at http://anna.fi.muni.cz/papers/src/public/5f773c95a13c7b85f303123b36985210.pdf.
J. Barnat, L. Brim & J. Chaloupka (2003):
Parallel Breadth-First Search LTL Model-Checking.
In: 18th IEEE International Conference on Automated Software Engineering (ASE'03).
IEEE Computer Society,
pp. 106–115,
doi:10.1109/ASE.2003.1240299.
J. Barnat, L. Brim & J. Chaloupka (2005):
From Distributed Memory Cycle Detection to Parallel LTL Model Checking.
Electronic Notes in Theoretical Computer Science 133(1),
pp. 21–39,
doi:10.1016/j.entcs.2004.08.056.
J. Barnat, L. Brim & P. Ročkai (2007):
Scalable Multi-core LTL Model-Checking.
In: Model Checking Software,
LNCS 4595.
Springer,
pp. 187–203,
doi:10.1007/978-3-540-73370-6_13.
J. Barnat, L. Brim & P. Ročkai (2008):
DiVinE Multi-Core – A Parallel LTL Model-Checker.
In: Automated Technology for Verification and Analysis (ATVA 2008),
LNCS 5311.
Springer,
pp. 234–239,
doi:10.1007/978-3-540-88387-6_20.
J. Barnat, L. Brim & P. Ročkai (2009):
A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties.
In: Formal Methods and Software Engineering (ICFEM 2009),
LNCS 5885.
Springer,
pp. 407–425,
doi:10.1007/978-3-642-10373-5_21.
J. Barnat, L. Brim & P. Ročkai (2010):
Parallel Partial Order Reduction with Topological Sort Proviso.
In: Software Engineering and Formal Methods (SEFM 2010).
IEEE Computer Society Press,
pp. 222–231,
doi:10.1109/SEFM.2010.35.
J. Barnat, L. Brim & J. Stř\'ıbrná (2001):
Distributed LTL Model-Checking in SPIN.
In: Proc. SPIN Workshop on Model Checking of Software,
LNCS 2057.
Springer,
pp. 200–216,
doi:10.1007/3-540-45139-0_13.
J. Barnat, L. Brim, I. Černá, P. Moravec, P. Ročkai & P. Šimeček (2006):
DiVinE – A Tool for Distributed Verification (Tool Paper).
In: Computer Aided Verification,
LNCS 4144/2006.
Springer Berlin / Heidelberg,
pp. 278–281,
doi:10.1007/11817963_26.
J. Barnat, L. Brim & M. Češka (2009):
DiVinE-CUDA: A Tool for GPU Accelerated LTL Model Checking.
Electronic Proceedings in Theoretical Computer Science (PDMC 2009) 14,
pp. 107–111,
doi:10.4204/EPTCS.14.8.
J. Barnat, L. Brim, M. Češka & T. Lamr (2009):
CUDA accelerated LTL Model Checking.
In: 15th International Conference on Parallel and Distributed Systems (ICPADS 2009).
IEEE Computer Society,
pp. 34–41,
doi:10.1109/ICPADS.2009.50.
J. Barnat, L. Brim, M. Češka & P. Ročkai (2010):
DiVinE: Parallel Distributed Model Checker (Tool paper).
In: Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology (HiBi/PDMC 2010).
IEEE,
pp. 4–7,
doi:10.1109/PDMC-HiBi.2010.9.
J. Barnat, L. Brim & P. Šimeček (2007):
I/O Efficient Accepting Cycle Detection.
In: Computer Aided Verification,
LNCS 4590.
Springer,
pp. 281–293,
doi:10.1007/978-3-540-73368-3_32.
J. Barnat, L. Brim, P. Šimeček & M. Weber (2008):
Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking.
In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS).,
LNCS 4963.
Springer,
pp. 48–62,
doi:10.1007/978-3-540-78800-3_5.
J. Barnat & P. Ročkai (2008):
Shared Hash Tables in Parallel Model Checking.
ENTCS 198(1),
pp. 79–91,
doi:10.1016/j.entcs.2007.10.021.
G. Behrmann, T. S. Hune & F. W. Vaandrager (2000):
Distributed Timed Model Checking — How the Search Order Matters.
In: Proc. 12th Conference on Computer-Aided Verification CAV00,
LNCS 1855.
Springer,
pp. 216–231,
doi:10.1007/10722167_19.
Armin Biere, Cyrille Artho & Viktor Schuppan (2002):
Liveness Checking as Safety Checking.
Electronic Notes in Theoretical Computer Science 66(2),
pp. 160 – 177,
doi:10.1016/S1571-0661(04)80410-9.
Brad Bingham, Jesse Bingham, Flavio M. de Paula, John Erickson, Gaurav Singh & Mark Reitblatt (2010):
Industrial Strength Distributed Explicit State Model Checking.
In: Parallel and Distributed Methods in Verification, 2010 Ninth International Workshop on, and High Performance Computational Systems Biology, Second International Workshop on.
IEEE Computer Society,
pp. 28–36,
doi:10.1109/PDMC-HiBi.2010.13.
D. Bosnacki, S. Edelkamp & D. Sulewski (2009):
Efficient Probabilistic Model Checking on General Purpose Graphics Processors.
In: Model Checking Software (SPIN 2009),
LNCS 5578.
Springer,
pp. 32–49,
doi:10.1007/978-3-642-02652-2_7.
L. Brim, I. Černá, P. Moravec & J. Šimša (2004):
Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking.
In: Formal Methods in Computer Aided Design (FMCAD),
LNCS 4144.
Springer,
pp. 352–366,
doi:10.1007/978-3-540-30494-4_25.
L. Brim, I. Černá, P. Krčál & R. Pelánek (2001):
Distributed LTL Model Checking Based on Negative Cycle Detection.
In: Proc. of Foundations of Software Technology and Theoretical Computer Science (FST TCS 2001),
LNCS 2245.
Springer,
pp. 96–107,
doi:10.1007/3-540-45294-X_9.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill & L. J. Hwang (1992):
Symbolic Model Checking: 10^20 States and Beyond.
Information and Computation 98(2),
pp. 142–170.
Available at http://citeseer.nj.nec.com/burch92symbolic.html.
S. Caselli, G. Conte & P. Marenzoni (1995):
Parallel state space exploration for GSPN models.
In: G. de Michelis & M. Diaz: Applications and Theory of Petri Nets 1995,
LNCS 935.
Springer Verlag,
pp. 181–200,
doi:10.1007/3-540-60029-9_40.
I. Černá & R. Pelánek (2003):
Distributed Explicit Fair Cycle Detection.
In: Model Checking Software, 10th International SPIN Workshop,
LNCS 2648.
Springer,
pp. 49–73,
doi:10.1007/3-540-44829-2_4.
I. Černá & R. Pelánek (2003):
Relating Hierarchy of Temporal Properties to Model Checking.
In: Mathematical Foundations of Computer Science (MFCS),
LNCS 2747.
Springer,
pp. 318–327,
doi:10.1007/978-3-540-45138-9_26.
Yi-Jen Chiang, Michael T. Goodrich, Edward F. Grove, Roberto Tamassia, Darren Erik Vengroff & Jeffrey Scott Vitter (1995):
External-memory graph algorithms.
In: soda.
Society for Industrial and Applied Mathematics,
pp. 139–149,
doi:10.1145/313651.313681.
G. Ciardo, J. Gluckman & D.M. Nicol (1998):
Distributed State Space Generation of Discrete-State Stochastic Models.
INFORMS Journal on Computing 10(1),
pp. 82–93,
doi:10.1287/ijoc.10.1.82.
Gianfranco Ciardo (1997):
Automated parallelization of discrete state-space generation.
J. Parallel Distrib. Comput. 47,
pp. 153–167,
doi:10.1006/jpdc.1997.1409.
E. M. Clarke, R. Enders, T. Filkorn & S. Jha (1996):
Exploiting symmetry in temporal logic model checking.
Form. Methods Syst. Des. 9(1-2),
pp. 77–104,
doi:10.1007/BF00625969.
E.M. Clarke, O. Grumberg, S. Jha, Y. Lu & H. Veith (2001):
Progress on the State Explosion Problem in Model Checking.
In: R. Wilhelm: Informatics - 10 Years Back. 10 Years Ahead,
LNCS 2000.
Springer,
pp. 176–194.
(2009):
NVIDIA CUDA Compute Unified Device Architecture - Programming Guide Version 2.0,.
http://www.nvidia.com/object/cuda_develop.html, June 2009.
David L. Dill (1996):
The Murφ verification system.
In: Conference on Computer-Aided Verification (CAV'96),
LNCS.
Springer-Verlag,
pp. 390–393.
Available at http://dl.acm.org/citation.cfm?id=647765.735832.
Stefan Edelkamp, Peter Sanders & Pavel Šimeček (2008):
Semi-external LTL Model Checking.
In: Computer Aided Verification (CAV 2008).
Springer,
Berlin, Heidelberg,
pp. 530–542,
doi:10.1007/978-3-540-70545-1_50.
Stefan Edelkamp & Damian Sulewski (2008):
Model Checking via Delayed Duplicate Detection on the GPU..
Technical Report Technical Report 821.
TU Dortmund.
Available at http://www.tzi.de/~edelkamp/GPU_Technical.pdf.
Presented on the 22nd Workshop on Planning, Scheduling, and Design PUK 2008.
T. von Eicken, D. E. Culler, S. C. Goldstein & K. E. Schauser (1992):
Active messages: a mechanism for integrated communication and computation.
In: 19th Annual International Symposium on Computer Architecture,
pp. 256–266,
doi:10.1145/285930.286002.
E. Allen Emerson & A. Prasad Sistla (1996):
Symmetry and model checking.
Form. Methods Syst. Des. 9(1-2),
pp. 105–131,
doi:10.1007/BF00625970.
Sami Evangelista (2008):
Dynamic Delayed Duplicate Detection for External Memory Model Checking.
In: SPIN '08: Proc. of the 15th international workshop on Model Checking Software.
Springer,
Berlin, Heidelberg,
pp. 77–94,
doi:10.1007/978-3-540-85114-1_8.
H. Garavel, R. Mateescu & I.M Smarandache (2001):
Parallel State Space Construction for Model-Checking.
In: Matthew B. Dwyer: Model Checking of Software (SPIN'2001),
LNCS 2057.
Springer-Verlag,
pp. 216–234,
doi:10.1007/3-540-45139-0_14.
Jaco Geldenhuys & P. J. A. de Villiers (1999):
Runtime Efficient State Compaction in SPIN.
In: SPIN,
pp. 12–21,
doi:10.1007/3-540-48234-2_2.
Naga K. Govindaraju, Jim Gray, Ritesh Kumar & Dinesh Manocha (2006):
GPUTeraSort: high performance graphics co-processor sorting for large database management.
In: International Conference on Management of Data (SIGMOD 06).
ACM,
pp. 325–336,
doi:10.1145/1142473.1142511.
Moritz Hammer & Michael Weber (2006):
"To Store or Not To Store" Reloaded: Reclaiming Memory on Demand.
In: Formal Methods: Applications and Technology,
LNCS 4346.
Springer,
pp. 51–66,
doi:10.1007/978-3-540-70952-7_4.
P. Harish & P. J. Narayanan (2007):
Accelerating Large Graph Algorithms on the GPU Using CUDA.
In: HiPC,
LNCS 4873.
Springer,
pp. 197–208,
doi:10.1007/978-3-540-77220-0_21.
P. Harish, V. Vineet & P. J. Narayanan (2009):
Large Graph Algorithms for Massively Multithreaded Architectures.
Technical Report IIIT/TR/2009/74.
Center for Visual Information Technology, International Institute of Information Technology Hyderabad, INDIA.
Available at http://cvit.iiit.ac.in/papers/pawan09GraphAlgorithms.pdf.
M. Harris:
Optimizing Parallel Reduction in CUDA,.
http://developer.download.nvidia.com/compute/cuda/1_1/Website/projects/reduction/doc/reduction.pdf, March 2010.
B. R. Haverkort, A. Bell & H. C. Bohnenkamp (1999):
On the efficient sequential and distributed generation of very large Markov chains from stochastic Petri nets..
In: Petri Net and Performance Models (PNPM'99).
IEEE Computer Society Press,
pp. 12–21,
doi:10.1109/PNPM.1999.796528.
Boudewijn R. Haverkort, Henrik Bohnenkamp & Alexander Bell (1998):
Efficiency Improvements in the Evaluation of Large Stochastic Petri Nets.
In: Forschungsbericht: 5. Workshop Algorithmen und Werkzeuge f\IeC ür Petrinetze.
Universit\IeC ät Dortmund, Fachbereich Informatik,
pp. 55–61.
Available at http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.41.3435&rep=rep1&type=pdf.
Keijo Heljanko, Victor Khomenko & Maciej Koutny (2002):
Parallelisation of the Petri Net Unfolding Algorithm.
In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2002),
LNCS 2280.
Springer,
pp. 371–385,
doi:10.1007/3-540-46002-0_26.
Gerard J. Holzmann (2003):
The Spin Model Checker: Primer and Reference Manual.
Addison-Wesley.
Gerard J. Holzmann (2008):
A Stack-Slicing Algorithm for Multi-Core Model Checking.
ENTCS 198(1),
pp. 3–16,
doi:10.1016/j.entcs.2007.10.017.
Gerard J. Holzmann & Dragan Bosnacki (2007):
The Design of a Multicore Extension of the SPIN Model Checker.
IEEE Trans. Software Eng. 33(10),
pp. 659–674,
doi:10.1109/TSE.2007.70724.
Cornelia P. Inggs & Howard Barringer (2005):
CTL^* Model Checking on a Shared-Memory Architecture.
Electronic Notes in Theoretical Computer Science 128(3),
pp. 107–123,
doi:10.1016/j.entcs.2004.10.022.
Shahid Jabbar & Stefan Edelkamp (2005):
I/O Efficient Directed Model Checking.
In: Verification, Model Checking, and Abstract Interpretation (VMCAI 2005),
LNCS 3385.
Springer,
pp. 313–329,
doi:10.1007/978-3-540-30579-8_21.
Shahid Jabbar & Stefan Edelkamp (2006):
Parallel External Directed Model Checking with Linear I/O.
In: Verification, Model Checking, and Abstract Interpretation (VMCAI 2006),
LNCS 3855.
Springer,
pp. 237–251,
doi:10.1007/11609773_16.
G. Jayachandran, V. Vishal & V. S. Pande (2006):
Using massively parallel simulations and Markovian models to study protein folding: examining the villin head-piece.
Journal of Chemical Physics 124(6),
pp. 903\IeC 914,
doi:10.1063/1.2186317.
Michael Jones & Eric Mercer (2004):
Explicit State Model Checking with Hopper.
In: Model Checking Software (SPIN 2004),
Lecture Notes in Computer Science 2989.
Springer,
pp. 146–150,
doi:10.1007/978-3-540-24732-6_10.
A. B. Kahn (1962):
Topological sorting of large networks.
Communications of the ACM 5(11),
pp. 558–562.
W. Knottenbelt, P.G Harrison, M. Mestern & P.S. Kritzinger (2000):
A Probabilistic Dynamic Technique for the Distributed Generation of Very Large State Spaces.
Performance Evaluation 35(1–4),
pp. 127–148,
doi:10.1016/S0166-5316(99)00061-9.
W. Knottenbelt, M. Mestern, P.G Harrison & P.S. Kritzinger (1998):
Probability, Parallelism and the State Space Exploration Problem.
In: R. Puigjaner: Tools'98,
LNCS 1469.
Springer Verlag,
pp. 165–179,
doi:10.1007/3-540-68061-6_14.
R. Korf & P. Schultze (2005):
Large-Scale Parallel Breadth-First Search.
In: Proceedings of the 20th national conference on Artificial intelligence - Volume 3.
AAAI Press / The MIT Press,
pp. 1380–1385.
Available at http://dl.acm.org/citation.cfm?id=1619499.1619555.
Rahul Kumar & Eric G. Mercer (2005):
Load Balancing Parallel Explicit State Model Checking.
Electronic Notes in Theoretical Computer Science 128(3),
pp. 19–34,
doi:10.1016/j.entcs.2004.10.016.
Alfons Laarman, Jaco van de Pol & Michael Weber (2010):
Boosting Multi-Core Reachability Performance with Shared Hash Tables.
In: Formal Methods in Computer-Aided Design (FMCAD 2010).
IEEE,
pp. 247–255.
Available at http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=5770956.
Peter Lamborn & Eric A. Hansen (2008):
Layered Duplicate Detection in External-Memory Model Checking.
In: SPIN '08: Proc. of the 15th international workshop on Model Checking Software.
Springer,
Berlin, Heidelberg,
pp. 160–175,
doi:10.1007/978-3-540-85114-1_13.
Flavio Lerda & Riccardo Sisto (1999):
Distributed-memory Model Checking with SPIN.
In: Proc. of the 5th International SPIN Workshop,
LNCS 1680.
Springer-Verlag,
pp. 22–39,
doi:10.1007/3-540-48234-2_3.
Flavio Lerda & Willem Visser (2001):
Addressing Dynamic Issues of Program Model Checking.
In: International SPIN Workshop on Model Checking of Software (SPIN'2001),
LNCS 2057.
Springer,
pp. 80–102,
doi:10.1007/3-540-45139-0_6.
Ulrich Meyer, Peter Sanders & Jop Sibeyn (2003):
Algorithms for Memory Hierarchies.
Springer.
Doron Peled (1998):
Ten Years of Partial Order Reduction.
In: Proceedings of the 10th International Conference on Computer Aided Verification.
Springer-Verlag,
pp. 17–28.
R. Pel\IeC ánek (2009):
Fighting State Space Explosion: Review and Evaluation.
In: Formal Methods for Industrial Critical Systems (FMICS 2008),
LNCS 5596.
Springer,
pp. 37–52,
doi:10.1007/978-3-642-03240-0_7.
Giuseppe Della Penna, Benedetto Intrigila, Enrico Tronci & Marisa Venturini Zilli (2002):
Exploiting Transition Locality in the Disk Based Murφ Verifier.
In: Formal Methods in Computer-Aided Design (FMCAD 2002),
pp. 202–219,
doi:10.1007/3-540-36126-X_13.
U. Stern & D. L. Dill (1997):
Parallelizing the Murφ Verifier.
In: O. Grumberg: Proceedings of Computer Aided Verification (CAV '97),
LNCS 1254.
Springer-Verlag,
pp. 256–267,
doi:10.1007/BFb0028727.
U. Stern & D. L. Dill (1998):
Using Magnetic Disk Instead of Main Memory in the Murφ Verifier.
In: Computer Aided Verification. 10th International Conference,
pp. 172–183,
doi:10.1007/BFb0028743.
M.Y. Vardi & P. Wolper (1986):
An automata-theoretic approach to automatic program verification.
In: Proc. IEEE Symposium on Logic in Computer Science.
Computer Society Press,
pp. 322–331.
K. Verstoep, H. Bal, J. Barnat & L. Brim (2009):
Efficient Large-Scale Model Checking.
In: 23rd IEEE International Parallel & Distributed Processing Symposium (IPDPS 2009).
IEEE,
pp. 1–12,
doi:10.1109/IPDPS.2009.5161000.
Rong Zhou & Eric A. Hansen (2004):
Structured Duplicate Detection in External-Memory Graph Search.
In: AAAI.
AAAI Press / The MIT Press,
pp. 683–689.
Available at http://www.aaai.org/Papers/AAAI/2004/AAAI04-108.pdf.