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.
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).
"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).
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
.
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.
Symbolic Reachability Analysis based on SAT-Solvers
, Master's Thesis,
Niklas Eén, 1999.
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.
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.