-
Verifying Reachability Properties in Markov Chains via Incremental Induction
Authors:
Elizabeth Polgreen,
Martin Brain,
Martin Fraenzle,
Alessandro Abate
Abstract:
There is a scalability gap between probabilistic and non-probabilistic verification. Probabilistic model checking tools are based either on explicit engines or on (Multi-Terminal) Binary Decision Diagrams. These structures are complemented in areas of non-probabilistic verification by more scalable techniques, such as IC3. We present a symbolic probabilistic model checking algorithm based on IC3-l…
▽ More
There is a scalability gap between probabilistic and non-probabilistic verification. Probabilistic model checking tools are based either on explicit engines or on (Multi-Terminal) Binary Decision Diagrams. These structures are complemented in areas of non-probabilistic verification by more scalable techniques, such as IC3. We present a symbolic probabilistic model checking algorithm based on IC3-like incremental construction of inductive clauses to partition the state space, interleaved with incremental construction of a system of linear inequalities. This paper compares our implementation to standard quantitative verification alternatives: our experiments show that our algorithm is a step to more scalable symbolic verification of rare events in finite-state Markov chains.
△ Less
Submitted 19 September, 2019; v1 submitted 17 September, 2019;
originally announced September 2019.
-
CVC4 at the SMT Competition 2018
Authors:
Clark Barrett,
Haniel Barbosa,
Martin Brain,
Duligur Ibeling,
Tim King,
Paul Meng,
Aina Niemetz,
Andres Nötzli,
Mathias Preiner,
Andrew Reynolds,
Cesare Tinelli
Abstract:
This paper is a description of the CVC4 SMT solver as entered into the 2018 SMT Competition. We only list important differences from the 2017 SMT Competition version of CVC4. For further and more detailed information about CVC4, please refer to the original paper, the CVC4 website, or the source code on GitHub.
This paper is a description of the CVC4 SMT solver as entered into the 2018 SMT Competition. We only list important differences from the 2017 SMT Competition version of CVC4. For further and more detailed information about CVC4, please refer to the original paper, the CVC4 website, or the source code on GitHub.
△ Less
Submitted 19 June, 2018;
originally announced June 2018.
-
Functional Requirements-Based Automated Testing for Avionics
Authors:
Youcheng Sun,
Martin Brain,
Daniel Kroening,
Andrew Hawthorn,
Thomas Wilson,
Florian Schanda,
Francisco Javier Guzman Jimenez,
Simon Daniel,
Chris Bryan,
Ian Broster
Abstract:
We propose and demonstrate a method for the reduction of testing effort in safety-critical software development using DO-178 guidance. We achieve this through the application of Bounded Model Checking (BMC) to formal low-level requirements, in order to generate tests automatically that are good enough to replace existing labor-intensive test writing procedures while maintaining independence from i…
▽ More
We propose and demonstrate a method for the reduction of testing effort in safety-critical software development using DO-178 guidance. We achieve this through the application of Bounded Model Checking (BMC) to formal low-level requirements, in order to generate tests automatically that are good enough to replace existing labor-intensive test writing procedures while maintaining independence from implementation artefacts. Given that existing manual processes are often empirical and subjective, we begin by formally defining a metric, which extends recognized best practice from code coverage analysis strategies to generate tests that adequately cover the requirements. We then formulate the automated test generation procedure and apply its prototype in case studies with industrial partners. In review, the method developed here is demonstrated to significantly reduce the human effort for the qualification of software products under DO-178 guidance.
△ Less
Submitted 5 July, 2017;
originally announced July 2017.
-
Satisfiability Checking meets Symbolic Computation (Project Paper)
Authors:
E. Abraham,
J. Abbott,
B. Becker,
A. M. Bigatti,
M. Brain,
B. Buchberger,
A. Cimatti,
J. H. Davenport,
M. England,
P. Fontaine,
S. Forrest,
A. Griggio,
D. Kroening,
W. M. Seiler,
T. Sturm
Abstract:
Symbolic Computation and Satisfiability Checking are two research areas, both having their individual scientific focus but sharing also common interests in the development, implementation and application of decision procedures for arithmetic theories. Despite their commonalities, the two communities are rather weakly connected. The aim of our newly accepted SC-square project (H2020-FETOPEN-CSA) is…
▽ More
Symbolic Computation and Satisfiability Checking are two research areas, both having their individual scientific focus but sharing also common interests in the development, implementation and application of decision procedures for arithmetic theories. Despite their commonalities, the two communities are rather weakly connected. The aim of our newly accepted SC-square project (H2020-FETOPEN-CSA) is to strengthen the connection between these communities by creating common platforms, initiating interaction and exchange, identifying common challenges, and develo** a common roadmap from theory along the way to tools and (industrial) applications. In this paper we report on the aims and on the first activities of this project, and formalise some relevant challenges for the unified SC-square community.
△ Less
Submitted 27 July, 2016;
originally announced July 2016.
-
Satisfiability Checking and Symbolic Computation
Authors:
E. Abraham,
J. Abbott,
B. Becker,
A. M. Bigatti,
M. Brain,
B. Buchberger,
A. Cimatti,
J. H. Davenport,
M. England,
P. Fontaine,
S. Forrest,
A. Griggio,
D. Kroening,
W. M. Seiler,
T. Sturm
Abstract:
Symbolic Computation and Satisfiability Checking are viewed as individual research areas, but they share common interests in the development, implementation and application of decision procedures for arithmetic theories. Despite these commonalities, the two communities are currently only weakly connected. We introduce a new project SC-square to build a joint community in this area, supported by a…
▽ More
Symbolic Computation and Satisfiability Checking are viewed as individual research areas, but they share common interests in the development, implementation and application of decision procedures for arithmetic theories. Despite these commonalities, the two communities are currently only weakly connected. We introduce a new project SC-square to build a joint community in this area, supported by a newly accepted EU (H2020-FETOPEN-CSA) project of the same name. We aim to strengthen the connection between these communities by creating common platforms, initiating interaction and exchange, identifying common challenges, and develo** a common roadmap. This abstract and accompanying poster describes the motivation and aims for the project, and reports on the first activities.
△ Less
Submitted 23 July, 2016;
originally announced July 2016.
-
Safety Verification and Refutation by k-invariants and k-induction (extended version)
Authors:
Martin Brain,
Saurabh Joshi,
Daniel Kroening,
Peter Schrammel
Abstract:
Most software verification tools can be classified into one of a number of established families, each of which has their own focus and strengths. For example, concrete counterexample generation in model checking, invariant inference in abstract interpretation and completeness via annotation for deductive verification. This creates a significant and fundamental usability problem as users may have t…
▽ More
Most software verification tools can be classified into one of a number of established families, each of which has their own focus and strengths. For example, concrete counterexample generation in model checking, invariant inference in abstract interpretation and completeness via annotation for deductive verification. This creates a significant and fundamental usability problem as users may have to learn and use one technique to find potential problems but then need an entirely different one to show that they have been fixed. This paper presents a single, unified algorithm kIkI, which strictly generalises abstract interpretation, bounded model checking and k-induction. This not only combines the strengths of these techniques but allows them to interact and reinforce each other, giving a `single-tool' approach to verification.
△ Less
Submitted 29 June, 2015; v1 submitted 18 June, 2015;
originally announced June 2015.
-
Incremental Bounded Model Checking for Embedded Software (extended version)
Authors:
Peter Schrammel,
Daniel Kroening,
Martin Brain,
Ruben Martins,
Tino Teige,
Tom Bienmüller
Abstract:
Program analysis is on the brink of mainstream in embedded systems development. Formal verification of behavioural requirements, finding runtime errors and automated test case generation are some of the most common applications of automated verification tools based on Bounded Model Checking. Existing industrial tools for embedded software use an off-the-shelf Bounded Model Checker and apply it ite…
▽ More
Program analysis is on the brink of mainstream in embedded systems development. Formal verification of behavioural requirements, finding runtime errors and automated test case generation are some of the most common applications of automated verification tools based on Bounded Model Checking. Existing industrial tools for embedded software use an off-the-shelf Bounded Model Checker and apply it iteratively to verify the program with an increasing number of unwindings. This approach unnecessarily wastes time repeating work that has already been done and fails to exploit the power of incremental SAT solving. This paper reports on the extension of the software model checker CBMC to support incremental Bounded Model Checking and its successful integration with the industrial embedded software verification tool BTC EmbeddedTester. We present an extensive evaluation over large industrial embedded programs, which shows that incremental Bounded Model Checking cuts runtimes by one order of magnitude in comparison to the standard non-incremental approach, enabling the application of formal verification to large and complex embedded software.
△ Less
Submitted 20 September, 2014;
originally announced September 2014.
-
Automatic Music Composition using Answer Set Programming
Authors:
Georg Boenn,
Martin Brain,
Marina De Vos,
John ffitch
Abstract:
Music composition used to be a pen and paper activity. These these days music is often composed with the aid of computer software, even to the point where the computer compose parts of the score autonomously. The composition of most styles of music is governed by rules. We show that by approaching the automation, analysis and verification of composition as a knowledge representation task and forma…
▽ More
Music composition used to be a pen and paper activity. These these days music is often composed with the aid of computer software, even to the point where the computer compose parts of the score autonomously. The composition of most styles of music is governed by rules. We show that by approaching the automation, analysis and verification of composition as a knowledge representation task and formalising these rules in a suitable logical language, powerful and expressive intelligent composition tools can be easily built. This application paper describes the use of answer set programming to construct an automated system, named ANTON, that can compose melodic, harmonic and rhythmic music, diagnose errors in human compositions and serve as a computer-aided composition tool. The combination of harmonic, rhythmic and melodic composition in a single framework makes ANTON unique in the growing area of algorithmic composition. With near real-time composition, ANTON reaches the point where it can not only be used as a component in an interactive composition tool but also has the potential for live performances and concerts or automatically generated background music in a variety of applications. With the use of a fully declarative language and an "off-the-shelf" reasoning engine, ANTON provides the human composer a tool which is significantly simpler, more compact and more versatile than other existing systems. This paper has been accepted for publication in Theory and Practice of Logic Programming (TPLP).
△ Less
Submitted 25 June, 2010;
originally announced June 2010.
