Selected Publications of Dennis Dams

The following list of publications is sorted by topic (Model Checking & Temporal Logic / Logic Programming). Within each of these topics, the publications are sorted by type (In journals / In proceedings / Technical reports / Thesis / Other). For most papers, more information is available, like abstracts, BIBTeX entries, PostScript sources, information about earlier versions, etc.

If you have any comments or questions about this page, please send email to the address found on my home page.

Model Checking & Temporal Logic

In journals

DLS02a

with Yassine Lakhnech and Martin Steffen. Iterating transducers. Journal of Logic and Algebraic Programming, 52-53:109-127, Elsevier, 2002. A previous version of this article has occurred in Computer Aided Verification, number 2102 in LNCS, pages 286-297, © Springer, 2001.

BDH02a

with Dragan Bošnački and Leszek Holenderski. Symmetric SPIN. International Journal on Software Tools for Technology Transfer, 4(1):92-106, © Springer, 2002.

Dam99a

Flat fragments of CTL and CTL*: Separating the expressive and distinguishing powers. Logic Journal of the IGPL, 7(1):55-78, © Oxford University Press, 1999.

DGKK98b

with Rob Gerth, Bart Knaack, and Ruurd Kuiper. Partial-order reduction techniques for real-time model checking. Formal Aspects of Computing, (10):469-482, Springer, 1998. (preliminary version available)

DGG97

with Rob Gerth and Orna Grumberg. Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems, 19(2):253-291, 1997. (preliminary version available)

Editorship

DGLM99

with Rob Gerth, Stefan Leue, and Mieke Massink, editors. Theoretical and Practical Aspects of SPIN Model Checking. Number 1680 in LNCS. Springer, Berlin, 1999.

In proceedings

CNDE05a

with Christopher L. Conway, Kedar S. Namjoshi, and Stephen A. Edwards. Incremental Algorithms for Inter-procedural Analysis of Safety Properties. In Kousha Etessami and Sriram K. Rajamani, editors, Computer Aided Verification, number 3576 in Lecture Notes in Computer Science, pages 449-461, Springer, Berlin, 2005. © Springer. Bell Labs techreport ITD-05-46458Y, Oct. 3, 2005.

DN05a

with Kedar S. Namjoshi. Automata as Abstractions. In Radhia Cousot, editor, Verification, Model Checking, and Abstract Interpretation, number 3385 in Lecture Notes in Computer Science, pages 216-232, Springer, Berlin, 2005. © Springer.

DN04a

with Kedar S. Namjoshi. The existence of finite abstractions for branching time model checking. In Nineteenth Annual IEEE Symposium on Logic in Computer Science (LICS'04), pages 335--344, Los Alamitos, CA, 2004. IEEE TC-MFC, IEEE Computer Society Press. © IEEE.

Dam03a

Comparing abstraction refinement algorithms. Workshop on Software Model Checking, Boulder, CO, July 2003. Electronic Notes in Computer Science, vol. 89(3). Elsevier.

DN03a

with Kedar S. Namjoshi. Shape analysis through predicate abstraction and model checking. In Verification, Model Checking, and Abstract Interpretation (VMCAI), number 2575 in LNCS, pages 310--323. © Springer, 2003.

PMH+02a

with P. Pingree, E. Mikk, G. Holzmann, and M. Smith. Validation of mission critical software design and implementation using model checking. In The 21st Digital Avionics Systems Conference, October 2002.

Dam02a

Abstraction in software model checking: Principles and practice (tutorial overview and bibliography). In Dragan Bošnački and Stefan Leue, editors, Model Checking Software, number 2318 in LNCS. © Springer, 2002.
(presentation - 3.5MB, version without cartoons - 800KB)

DHH02a

with William Hesse and Gerard Holzmann. Abstracting C with abC. In Ed Brinksma and Kim Guldstrand Larsen, editors, Computer Aided Verification, number 2404 in LNCS, pages 515--520. © Springer, 2002.

BDH00a

with Dragan Bošnački and Leszek Holenderski. A heuristic for symmetry reductions with scalarsets. In J.N. Oliveira and P. Zave, editors, FME 2001: Formal Methods for Increasing Software Productivity, number 2021 in LNCS, pages 518--533. © Springer, Berlin, 2001.

GD00a

with Marc Geilen. An on-the-fly tableau construction for a real-time temporal logic. In M. Joseph, editor, Proceedings of the Sixth International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT2000, 20--22 September, 2000, Pune, India, number 1926 in LNCS, pages 276-290. © Springer, Berlin, 2000.

DGG00b

with Rob Gerth and Orna Grumberg. Fair model checking of abstractions (extended abstract). In Michael Leuschel, Andreas Podelski, C.R. Ramakrishnan, and Ulrich Ultes-Nitsche, editors, Proceedings of the Workshop on Verification and Computational Logic (VCL'2000), number DSSE-TR-2000-6, University of Southampton, July 2000.

DGG00a

with Rob Gerth and Orna Grumberg. A heuristic for the automatic generation of ranking functions. In Ganesh Gopalakrishnan, editor, Workshop on Advances in Verification (WAVe'00), pages 1-8, School of Computing, university of Utah, July 2000.

BDHS00a

with Dragan Bošnački, Leszek Holenderski, and Natalia Sidorova. Model checking SDL with Spin. In Susanne Graf and Michael Schwartzbach, editors, Tools and Algorithms for the Construction and Analysis of Systems, number 1785 in LNCS, pages 363-377. © Springer, Berlin, 2000.

DHS99a

with Dieter Hutter and Natalia Sidorova. Using the INKA prover to automate safety proofs in abstract interpretation - A case study. Abstract. In Françoise Bellegarde and Olga Kouchnarenko, editors, Workshop on Modelling and Verification, C.I.S., Besançon, France, 1999.

GVD98a

with M.C.W. Geilen and J.P.M. Voeten. Applying verification methods to non-exhaustive verification of software/hardware systems. In Proceedings CSSP98 + SAFE98, pages 177--183. ProRISC, 1998. Also see the poster.

BD98b

with D. Bošnački. Discrete-time Promela and Spin. In Anders P. Ravn and Hans Rischel, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems, number 1486 in LNCS, pages 307--310. © Springer, Berlin, 1998.

BD98a

with D. Bošnački. Integrating real time into Spin: A prototype implementation. In Stan Budkowski, Ana Cavalli, and Elie Najm, editors, Formal Description Techniques and Protocol Specification, Testing and Verification (FORTE/PSTV), pages 423--438, Paris, France, October 1998. IFIP.

DG97a

with Rob Gerth. The bounded retransmission protocol revisited (extended abstract). In Faron Moller, editor, Second International Workshop on Verification of Infinite State Systems (Infinity'97), volume 9 of Electronic Notes in Theoretical Computer Science. © Elsevier Science Publishers B.V. (North-Holland), 1997.

DGFK97

with Rob Gerth, Loe Feijs and Gertjan Kamsteeg. Experiences with modelling the USB hub protocol using Spin. In Ignac Lovrek, editor, Applied Formal Methods in System Design, proceedings of the 2nd International Workshop, pages 147-158, HR-10000, Unska 3, Zagreb, Croatia, June 1997. European research action COST 247 and the University of Zagreb.

DGDHKP94

with Rob Gerth, Gert Döhmen, Ronald Herrmann, Peter Kelb, and Hergen Pargmann. Model checking using adaptive state and data abstraction. In David L. Dill, editor, Computer Aided Verification, number 818 in Lecture Notes in Computer Science, pages 455-467, Springer-Verlag, Berlin, 1994.

DGG94a

with Orna Grumberg and Rob Gerth. Abstract interpretation of reactive systems: Abstractions preserving ACTL*, ECTL* and CTL*. In E.-R. Olderog, editor, Proceedings of the IFIP WG2.1/WG2.2/WG2.3 Working Conference on Programming Concepts, Methods and Calculi (PROCOMET), IFIP Transactions, North-Holland/Elsevier, Amsterdam, 1994.
Technical report versions: DGG94, DGG95a. These are superseded by Chapter 4 of my PhD thesis (Dam96).

DGG93

with Rob Gerth and Orna Grumberg. Generation of reduced models for checking fragments of CTL. In Costas Courcoubetis, editor, Computer Aided Verification, number 697 in Lecture Notes in Computer Science, pages 479-490, Springer-Verlag, Berlin, 1993.

Technical reports / unpublished

DN04c

with Kedar S. Namjoshi. Orion: High-Precision Methods for Static Error Analysis of C and C++ Programs. Bell Labs Technical Memorandum ITD-04-45263Z. April 2004. © Lucent Technologies. Revised version submitted for publication.

DHS00a

with Dieter Hutter and Natalia Sidorova. Combining Theorem Proving and Model Checking --- A Case Study.

DG95

with Jan Friso Groote. Specification and implementation of components of a µCRL toolbox. Logic Group Preprint Series 152, Utrecht University, Dept. of Philosophy, Heidelberglaan 8, 3584 CS Utrecht, The Netherlands, December 1995.

KDG95

with Peter Kelb and Rob Gerth. Efficient symbolic model checking of the full µ-calculus using compositional abstractions. Computing Science Reports 95/31, Eindhoven University of Technology, P.O. Box 513, 5600 MB Eindhoven, The Netherlands, October 1995.

PhD Thesis

Dam96 (.ps, .pdf)

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. © D. Dams.
Some errata and the list of "stellingen" (in Dutch).

Other

Dam00a

Model checking toetst correctheid communicatieprotocol. PT Embedded Systems. © Ten Hagen & Stam Uitgevers, januari/februari 2000. In Dutch.

Logic Programming

In journals

CDFB96

with Michael Codish, Gilberto Filé, and Maurice Bruynooghe. On the design of a correct freeness analysis for logic programs. Journal of Logic Programming, 28(3):181--206, September 1996. © Elsevier Science.

CDY94

with Michael Codish and Eyal Yardeni. Bottom-up abstract interpretation of logic programs. Journal of Theoretical Computer Science, 124:93-125, February 1994. © ACM.

In proceedings

CDFB93

with Michael Codish, Gilberto Filé, and Maurice Bruynooghe. Freeness analysis for logic programs -- and correctness?. Logic Programming. Proceedings of the Tenth International Conference, pages 161--131, The MIT Press, Cambridge, Mass., 1993.

CDY91

with Michael Codish and Eyal Yardeni. Derivation and safety of an abstract unification algorithm for groundness and aliasing analysis. In Koichi Furukawa, editor, Logic Programming. Proceedings of the Eighth International Conference Logic Programming, pages 79-93, The MIT Press, Cambridge, Mass., 1991. © The Massachusetts Institute of Technology.

CDS90

with Michael Codish and Ehud Shapiro. Automatic detection of reply variables in concurrent logic programs. In M. Bruynooghe, editor, Proceedings of the Second Workshop on Meta-programming in Logic, pages 325--338, Leuven, Belgium, April 1990. K.U. Leuven, Department of Computer Science.

MSc Thesis

Dam90

Abstract interpretation of concurrent logic programs for analysis of variable sharing. Master's thesis, Eindhoven University of Technology, Dept. of Math. and Comp. Sc., P.O. Box 513, 5600 MB Eindhoven, The Netherlands, August 1990.