Literature:

Indications XXX of status has been added.

Testing and Debugging

(Ulrich) E. F. Moore: "Gedanken-experiments on sequential machines", Automata Studies. Princeton, JH: Princeton University Press. Ann. Math. Studies, no. 34, pp 129-153, 1956.

(Taken) David Lee, Mihalis Yannakakis: Principles and Methods of Testing Finite State Machines --- a Survey. Proceedings of the IEEE, vol 84, no 8, August 1996.

(Marius) S. Tripakis. Fault Diagnosis for Timed Automata. In FTRTFT, 2002.

Kim G. Larsen, Arne Skou:  Bisimulation through Probabilistic Testing, Information and Computation, vol 94, no 1, 1991. (I have preprints).

(Mandatory) H. Hong, I. Lee, O. Sokolsky, and H. Ural, "A Temporal Logic Based Theory of Test Coverage and Generation" International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS2002), April 8-11, 2002.

Elsa L. Gunter, Doron Peled: Temporal Debugging for Concurrent Systems. TACAS 2002: 431-444

Alex Groce, Doron Peled, Mihalis Yannakakis: Adaptive Model Checking. TACAS 2002: 357-370

Natasha Sharygina, Doron Peled: A Combined Testing and Verification Approach for Software Reliability. FME 2001: 611-628

Doron Peled, Moshe Y. Vardi, Mihalis Yannakakis: Black Box Checking. FORTE 1999: 225-240

(Taken) Brian Nielsen and Arne Skou. Automated Test Generation from Timed Automata. International Journal on Software Tools for Technology Transfer (STTT), 2002

(Jens Peter) Rance Cleaveland et al.: A theory of testing for soft real-time systems. To appear in Eighth International Conference on Software Engineering and Knowledge Engineering (SEKE '96), pages 474--479, Lake Tahoe, Nevada, June 1996. Knowledge Systems Institute, Skokie, Illinois.

Probabilistic Models

L. de Alfaro, M. Kwiatkowska, G. Norman, D. Parker, R. Segala. Symbolic Model Checking of Concurrent Probabilistic Processes Using MTBDDs and the Kronecker Representation. In TACAS 2000: 6th International Worskshop on Tools and Algorithms for the Construction and Analysis of Systems, Lectures Notes in Computer Science, Springer-Verlag, 2000. Postscript, PDF.

L. de Alfaro. Computing Minimum and Maximum Reachability Times in Probabilistic Systems . In CONCUR 99: 10th International Conference on Concurrency Theory, Lecture Notes in Computer Sciences, Springer Verlag, 1999. Postscript, PDF.

(Taken) Reachability Analysis of Probabilistic Systems by Successive Refinements , Pedro R. D'Argenio, Bertrand Jeannet, Henrik E. Jensen, and Kim G. Larsen. Accepted for PAPM-PROBMIV 2001

M. Bozga, O. Maler: On the Representation of Probabilities over Structured Domains .
in N. Halbwachs and D. Peled (Eds.), Proc. CAV'99 ,261-273, LNCS 1633, Springer, 1999.
[Abstract and Postscript]

Symbolic Model Checking for Probabilistic Processes. (with C. Baier, E. Clarke, V. Garmhausen-Hartonas and M. Ryan). In ICALP'97, LNCS 1256, © Springer Verlag. pp11. April 1997.

Symbolic Model Checking of Concurrent Probabilistic Systems Using MTBDDs and Simplex. (with G. Norman, D. Parker and R. Segala). pp14. Technical report CSR-99-1. Jan 1999. Superseded by TACAS'00

Symbolic Model Checking of Concurrent Probabilistic Processes Using MTBDDs and the Kronecker Representation. (with L. de Alfaro, G. Norman, D. Parker and R. Segala). Results In Proc. TACAS'2000, LNCS vol. 1785, © Springer Verlag. Jan 2000.

Verifying Randomized Distributed Algorithms with PRISM. (with G. Norman and D. Parker). In Proc. WAVe'2000 . June 2000.

(Mandatory) C. Baier, B. Engelen, M. Majster-Cederbaum: Deciding Bisimilarity and Similarity for Probabilistic Processes,  Lecture Notes in Computer Science, Vol. 1102, pp 38-49, 1996.

 PVS, Theorem Proving, Timed Systems

Mechanical Verification of Timed Automata: A Case Study, presented at the 1996 IEEE Real-Time Technology and Applications Symposium (RTAS'96), Boston, MA, June 1996.

Verifying Hybrid Systems Modeled as Timed Automata: A Case Study, by Myla Archer and Connie Heitmeyer, to be presented at the International Workshop on Hybrid and Real-Time Systems (HART'97), Grenoble, France, March 1997.

Experiments in Theorem Proving and Model Checking for Protocol Verification, Klaus Havelund and N. Shankar

For more see link here

Compositionality & Abstraction

Dennis Dams: Abstract Interpretation and Partition Refinement for Model Checking. PhD thesis, Eindhoven University of Technology, P.O. Box 513, 5600 MB Eindhoven, The Netherlands, July 1996. ( I have a copy of the thesis ).

Computing Abstractions of Infinite State Systems Compositionally and Automatically   .
S. Bensalem, Y Lakhnech and S. Owre. A conference version of this paper will paper in the proceedings of CAV'98 which will be published as an LNCS, Springer-Verlag. Copyright of the conference version is held by Springer.© Springer-Verlag.

Abstraction-based Model Checking using Modal Transition Systems (with Patrice Godefroid and Radha Jagadeesan); 16pp, March 2001; preliminary version of a paper to appear at Concur 2001.

Abstract , PostScript , PostScript (gzip'ed)
Jørn Lind-Nielsen, Henrik Reif Andersen, Gerd Behrmann, Henrik Hulgaard, Kåre Kristoffersen, Kim G. Larsen Verification of Large State/Event Systems using Compositionality and Dependency Analysis . Appears in Proceedings of TACAS'98, Bernhard Steffen (ed), LNCS 1384, April 1998. Springer-Verlag. NOTE: The technique described in this paper is being patented by Baan Visualstate (formerly Beologic) , which has all commercial rights
 

G. Behrmann, K. G. Larsen, H. R. Andersen, H. Hulgaard, J. Lind-Nielsen, " Verification of Hierarchical State/Event Systems using Reusability and Compositionality. " In Proceedings of TACAS'99. Springer-Verlag. NOTE: The technique described in this paper is being patented by Baan Visualstate , which has all commercial rights.

(Recommended) Orna Grumberg: Presentation at Marktoberdorf 2001.  Model Checking, Abstractions and Reductions

E.M.Clarke, O.Grumberg, D.E.Long:  `` Model Checking and Abstraction '',  ACM-TOPLAS, Vol. 16, No. 5, 1512- , September 1994.  

K.Yorav, O.Grumberg:
`` Static Analysis for State-Space Reductions Preserving Temporal Logics '',
TR #CS-2000-03, Computer Science Department, Technion, Israel (Submitted for publication).

Rance Cleaveland et all: Modeling and verifying active structural control systems Science of Computer Programming, 29(1-2):99-122, July 1997.

 (Mandatory) D. Bustan, O. Grumberg,"Simulation Based Minimization'', Inthe 17th International Conference on Automated Deduction (CADE'00), Pittsburgh, June 2000.

 

Symmetry Reduction

"Better Verification through Symmetry," C. Norris Ip and David L. Dill, Formal Methods in System Design, Volume 9, Numbers 1/2, pp 41-75, August 1996. (journal version).
 

BDDs, BEDs

The journal version of the above paper is "Boolean Expression Diagrams" by Henrik Reif Andersen and Henrik Hulgaard . To appear in Information and Computation . Available as PostScript (gzip'ed) , PostScript , and PDF .
 

SAT solving

Random 3-SAT and BDDs: The Plot Thickens Further (CP'01 paper Moshe Vardi, A. San Miguel Aguirre).

Chaff: Engineering an Efficient SAT Solver by M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, S. Malik, 39th Design Automation Conference, Las Vegas, June 2001.

Efficient Conflict Driven Learning in a Boolean Satisfiability Solver by L. Zhang, C. Madigan, M. Moskewicz, S. Malik, Accepted for publication, ICCAD 2001, San Jose, CA, Nov. 2001.

Mary Sheeran, Gunnar Stålmarck, a tutorial paper on Stålmarck's method of proof for propositional logic . The paper has now appeared in the journal Formal Methods in System Design, January 2000 issue. (we should get hold of this one).

Ordered Binary Decision Diagrams and the Davis-Putnam Procedure :
Tomas E. Uribe, Mark E. Stickel, 1994.

J. F. Groote:   The propositional formula checker HeerHugo .

Mary Sheeran, Satnam Singh: Checking safety properties using induction and a SAT-solver.
 
 

Bounded & Directed Model Checking

Symbolic Reachability Analysis based on SAT-Solvers , Master's Thesis, Niklas Eén, 1999.