Alcatel-Lucent > Bell Labs > Enabling Computing Technologies > Computing and Software Principles Research
Computing and Software Principles Research
Bell Labs

Dennis R. Dams

Bell Labs, Alcatel-Lucent
Copernicuslaan 50, D-6
B-2018 Antwerp, Belgium
Ph: +32-3-240-4415
Email: dennis research bell-labs com (insert one '@' and two '.'s)
Selected Publications
Last modified: Thu Mar 16 12:25:28 EST 2006

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).

Model Checking & Temporal Logic

In journals

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


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

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.
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.
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.
Comparing abstraction refinement algorithms. Workshop on Software Model Checking, Boulder, CO, July 2003. Electronic Notes in Computer Science, vol. 89(3). Elsevier.
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.
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.
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)
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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).
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

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.
with Dieter Hutter and Natalia Sidorova. Combining Theorem Proving and Model Checking --- A Case Study.
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.
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).


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

Logic Programming

In journals

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.
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

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.
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.
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

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.