Abstract. We present the tool MERIT, a CEGAR model-checker for safety propf counter-systems, which sits in the Lazy Abstraction with Interpolants (LAWI) framework. LAWI is parametr...
Testing of multi-threaded programs poses enormous challenges. To improve the coverage of testing, we present a framework named CONTESSA that augments conventional testing (concrete...
This paper discusses the obstacles that stand in the way of doing a good job of machine-code analysis. Compared with analysis of source code, the challenge is to drop all assumptio...
Thomas W. Reps, Junghee Lim, Aditya V. Thakur, Gog...
We introduce Petruchio, a tool for computing Petri net translations of dynamic networks. To cater for unbounded architectures beyond the capabilities of existing implementations, t...
Abstract. Concurrent data structures with fine-grained synchronization are notoriously difficult to implement correctly. The difficulty of reasoning about these implementations do...
Synthesis of program fragments from specifications can make programs easier to write and easier to reason about. We present Comfusy, a tool that extends the compiler for the gener...
We address the issue of automatic invariant synthesis for sequential programs manipulating singly-linked lists carrying data over infinite data doe define for that a framework ba...
Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, A...
We present a class of relaxed memory models, defined in Coq, parameterised by the chosen permitted local reorderings of reads and writes, and the visibility of inter- and intra-pr...
Jade Alglave, Luc Maranget, Susmit Sarkar, Peter S...