Projects per year
Abstract
Correctness of a program with respect to concurrency is often hard to achieve, but easy to specify: the concurrent program should produce the same results as a sequential reference version. We show how to automatically insert small atomic sections into a program to ensure correctness with respect to this implicit specification. Using techniques from bounded software model checking, we transform the program into an SMT formula that becomes unsatisfiable when we add correct atomic sections. By using uninterpreted functions to abstract data-related computational details, we make our approach applicable to programs with very complex computations, e.g., cryptographic algorithms. Our method starts with an empty set of atomic sections, and, based on counterexamples obtained from the SMT solver, refines the program by adding new atomic sections until correctness is achieved. We compare two different such refinement methods and provide experimental results, including Linux kernel modules where we successfully fix race conditions.
Original language | English |
---|---|
Title of host publication | Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design FMCAD 2014 |
Publisher | . |
Pages | 35-42 |
ISBN (Print) | 978-0-9835678-4-4 |
DOIs | |
Publication status | Published - 2014 |
Event | International Conference on Formal Methods in Computer-Aided Design - Lausanne, Switzerland Duration: 21 Oct 2014 → 24 Oct 2014 |
Conference
Conference | International Conference on Formal Methods in Computer-Aided Design |
---|---|
Country/Territory | Switzerland |
City | Lausanne |
Period | 21/10/14 → 24/10/14 |
Fields of Expertise
- Information, Communication & Computing
Treatment code (Nähere Zuordnung)
- Application
Fingerprint
Dive into the research topics of 'Synthesis of Synchronization using Uninterpreted Functions'. Together they form a unique fingerprint.Projects
- 3 Finished
-
FWF - QUAINT - Quantified Decision Procedures and Interpolation for Error Correction
Hofferek, G., Könighofer, R. & Bloem, R.
1/01/12 → 30/09/15
Project: Research project
-
FWF - RiSE - Rigorous Systems Engineering
Könighofer, R., Khalimov, A., Bloem, R., Könighofer, B. & Jacobs, S.
1/03/11 → 31/08/19
Project: Research project
-
Formal Methods for Design & Verification
Jacobs, S., Bloem, R., Könighofer, R., Könighofer, B., Khalimov, A., Hofferek, G. & Braud-Santoni, N.
1/02/08 → 15/07/19
Project: Research area