Damien Doligez
Gallium, Inria, Rocquencourt, France
-
A Concurrent, Generational Garbage Collector for a Multithreaded Implementation of ML
20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 1993 – POPL
This paper presents the design and implementation of a “quasi real-time” garbage collector for Concurrent Caml Light, an implementation of ML with threads. This two-generation system combines a fast, asynchronous copying collector on the young ...
bibtex -
Portable, Unobtrusive Garbage Collection for Multiprocessor Systems
POPL 1994: Portland, 1994 – POPL
We describe and prove the correctness of a new concurrent mark-and-sweep garbage collection algorithm. This algorithm derives from the classical on-the-fly algorithm from Dijkstra et al. [9]. A distinguishing feature of our algorithm is that it ...
bibtex -
A foundation for flow-based program matching: using temporal logic and model checking
36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, 2009 – POPL
Reasoning about program control-flow paths is an important functionality of a number of recent program matching languages and associated searching and transformation tools. Temporal logic provides a well-defined means of expressing properties of ...
bibtex -
A foundation for flow-based program matching: using temporal logic and model checking
ACM SIGPLAN Notices, vol. 44,no. 1,2009 – SIGPLAN_Notices
Reasoning about program control-flow paths is an important functionality of a number of recent program matching languages and associated searching and transformation tools. Temporal logic provides a well-defined means of expressing properties of ...
bibtex -
Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs
14th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR-14, vol. 4790,2007 – LPAR
We present Zenon, an automated theorem prover for first order classical logic (with equality), based on the tableau method. Zenon is intended to be the dedicated prover of the Focal environment, an object-oriented algebraic specification and proof ...
bibtex -
Hashconsing in an incrementally garbage-collected system: a story of weak pointers and hashconsing in ocaml 3.10.2
Proceedings of the ACM Workshop on ML, 2008 – ML
This article describes the implementations of weak pointers, weak hashtables and hashconsing in version 3.10.2 of the Objective Caml system, with focus on several performance pitfalls and their solutions.
bibtex -
bibtex
-
The TLA+ Proof System: Building a Heterogeneous Verification Platform
Oretical Aspects of Computing - ICTAC 2010, 7th International Colloquium, vol. 6255,2010 – International Colloquium on Theoretical Aspects of Computing
Model checking has proved to be an efficient technique for finding subtle bugs in concurrent and distributed algorithms and systems. However, it is usually limited to the analysis of small instances of such systems, due to the problem of state space ...
bibtex -
A TLA+ Proof System
Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, vol. 418,2008 – KEAPPA
bibtex -
Development of secured systems by mixing programs, specifications and proofs in an object-oriented programming environment: a case study within the FoCaLiZe environment
Proceedings of the 7th Workshop on Programming Languages and Analysis for Security, 2012 – PLAS
FoCaLiZe is an object-oriented programming environment that combines specifications, programs and proofs in the same language. This paper describes how its features can be used to formally express specifications and to develop by stepwise refinement ...
bibtex
