CAV
2010
Springer
13 years 9 months ago
2010
Springer
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...
CAV
2010
Springer
13 years 9 months ago
2010
Springer
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...
CAV
2010
Springer
13 years 9 months ago
2010
Springer
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...
CAV
2010
Springer
13 years 9 months ago
2010
Springer
CAV
2010
Springer
13 years 9 months ago
2010
Springer
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...
CAV
2010
Springer
13 years 9 months ago
2010
Springer
Abstract. Concurrent data structures with fine-grained synchronization are notoriously difficult to implement correctly. The difficulty of reasoning about these implementations do...
CAV
2010
Springer
13 years 9 months ago
2010
Springer
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...
CAV
2010
Springer
13 years 9 months ago
2010
Springer
CAV
2010
Springer
13 years 9 months ago
2010
Springer
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...
CAV
2010
Springer
13 years 9 months ago
2010
Springer
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...