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...
Abstract. This paper presents a practical automatic verification procedure for proving linearizability (i.e., atomicity and functional correctness) of concurrent data structure im...