Efficient Verification of Software with Replicated Components
Lead Research Organisation:
University of Oxford
Department Name: Computer Science
Abstract
Concurrency is a model of computation that allows many units of executionto coexist. It is ubiquitous in computer science today: user processes in atime-sharing operating system execute concurrently, as do worker threads ina client-server environment. Parallel processing, once primarily ofinterest in high-performance computing, has emerged in recent years as anew way of increasing processing power, such as in multi-core concurrentsystems, even for the home personal computer.Concurrency poses new challenges for the quality assurance of software, fortwo reasons. First, concurrent programs have the potential for forms oferrors unknown in sequential computation, such as race conditions andmutual exclusion violations. Second, traditional reliability measures suchas simulation and testing fail in the presence of concurrency, due to thedifficulties of reproducing erroneous behavior. Model Checking is anautomated technique to reliably establish the correctness of software, orto reveal the existence of errors in a reproducible manner. A program isrepresented by a finite-state model, which is exhaustively searched forviolations of pre-specified properties.Exhaustive search, however, generally incurs a cost proportional to thenumber of model states that are reached during the search. This number isin turn worst-case exponential in the number of concurrent components. Thisstate space explosion problem has been a major obstacle to the widespreaduse of model checking.One avenue of our research is guided by the observation that concurrentsystems often consist of replicated components: instances of a singletemplate, generically describing the behavior of each component. Concurrentsystems of replicated components often exhibit a veryregular---symmetric---structure: their behavior is invariant underinterchanges of the components. This causes redundancy in the system modeland in the (naive) exploration of the model's state space.We propose to investigate the efficacy of symmetry reduction andparameterized verification to attack the state space explosion problem forsoftware with replicated components. Both techniques have shown to betremendously effective in principle, namely due to their potential ofreducing the size of a symmetric system by an exponential factor, or ofcollapsing the verification problem for an infinite family of systems toone for a single system or a small finite family, respectively.The applicability of these techniques to concurrent software was hampered,however, by the apparent incapability of model checking to deal withinteger variables over very large domains or even unbounded, dynamic datastructures. The situation changed dramatically with the advent of automatedabstraction-refinement techniques. Software is initially representedabstractly using coarse finite-state models, risking the possibility ofincorrect---spurious---verification results. The new paradigm came withways of detecting spuriousness, and of dealing with it by iterativelyrefining the abstract model until spurious behavior is removed.To sum up, concurrent software exhibits two sources of complexity: largevariable data domains and concurrency. Fortunately, these sources areorthogonal and can be attacked separately. This separation makes itpossible to apply symmetry reduction and parameterized techniques toconcurrent software, methods that target the concurrency aspect of statespace explosion. The ultimate goal of the proposed work is to combine thesemethods with iterative abstraction refinement to obtain verification toolsfor concurrent software that can seriously curb state space explosion atall levels.
Organisations
People |
ORCID iD |
Daniel Kroening (Principal Investigator) |
Publications
Wahl T
(2010)
A lazy approach to symmetry reduction
in Formal Aspects of Computing
Wahl T
(2010)
Replication and Abstraction: Symmetry in Automated Formal Verification
in Symmetry
Spagnuolo A
(2022)
Characterizing passenger-ship emissions: towards improved sustainability for MedMar fleet (gulf of Naples).
in Energy efficiency
Sarkar S
(2012)
Synchronising C/C++ and POWER
in ACM SIGPLAN Notices
Sarkar S
(2012)
Synchronising C/C++ and POWER
Kroening D
(2012)
Loop summarization using state and transition invariants
in Formal Methods in System Design
Kaiser A
(2014)
A Widening Approach to Multithreaded Program Verification
in ACM Transactions on Programming Languages and Systems
Kaiser A
(2012)
CONCUR 2012 - Concurrency Theory
Donaldson A
(2011)
SCRATCH a tool for automatic analysis of dma races
in ACM SIGPLAN Notices
Donaldson A
(2012)
Counterexample-guided abstraction refinement for symmetric concurrent programs
in Formal Methods in System Design
Donaldson A
(2011)
Automatic analysis of DMA races using model checking and k-induction
in Formal Methods in System Design
D'Silva V
(2014)
Abstract satisfaction
Cook B
(2013)
Ranking function synthesis for bit-vector relations
in Formal Methods in System Design
Chockler H
(2012)
Computing Mutation Coverage in Interpolation-Based Model Checking
in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
Brillout A
(2011)
An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
in Journal of Automated Reasoning
Brain M
(2014)
Programming Languages and Systems
Blanc N
(2010)
Race analysis for systemc using model checking
in ACM Transactions on Design Automation of Electronic Systems
Basler G
(2010)
Context-aware counter abstraction
in Formal Methods in System Design
Basler G
(2009)
Computer Aided Verification
Alglave J
(2013)
Programming Languages and Systems
Alglave J
(2011)
Programming Languages and Systems
Description | There exists an extensive range of applications for CBMC, the software tool developed by this grant, for full details see http://www.cprover.org/cbmc/applications.shtml. CBMC has been used in the automotive industry for checking functionality of software, for verification of C code in pacemakers, for analysing driver interactions with semi-autonomous vehicles, and for runtime verification in ultra-critical systems used in aircraft. |
First Year Of Impact | 2010 |
Sector | Digital/Communication/Information Technologies (including Software),Electronics,Energy,Healthcare,Manufacturing, including Industrial Biotechology,Security and Diplomacy,Transport |
Impact Types | Economic |
Description | European Research Council |
Amount | £1,098,069 (GBP) |
Funding ID | CPROVER |
Organisation | European Research Council (ERC) |
Sector | Public |
Country | Belgium |
Start | 09/2011 |
End | 11/2016 |