| 1. |
- Abdulla, Parosh Aziz, Professor, 1961-, et al.
(author)
-
Boosting Constrained Horn Solving by Unsat Core Learning
- 2024
-
In: Verification, Model Checking, and Abstract Interpretation. - : Springer Nature. - 9783031505232 - 9783031505249 ; , s. 280-302
-
Conference paper (peer-reviewed)abstract
- The Relational Hyper-Graph Neural Network (R-HyGNN) was introduced in [1] to learn domain-specific knowledge from program verification problems encoded in Constrained Horn Clauses (CHCs). It exhibits high accuracy in predicting the occurrence of CHCs in counterexamples. In this research, we present an R-HyGNN-based framework called MUSHyperNet. The goal is to predict the Minimal Unsatisfiable Subsets (MUSes) (i.e., unsat core) of a set of CHCs to guide an abstract symbolic model checking algorithm. In MUSHyperNet, we can predict the MUSes once and use them in different instances of the abstract symbolic model checking algorithm. We demonstrate the efficacy of MUSHyperNet using two instances of the abstract symbolic modelchecking algorithm: Counter-Example Guided Abstraction Refinement (CEGAR) and symbolic model-checking-based (SymEx) algorithms. Our framework enhances performance on a uniform selection of benchmarks across all categories from CHC-COMP, solving more problems (6.1% increase for SymEx, 4.1% for CEGAR) and reducing average solving time (13.3% for SymEx, 7.1% for CEGAR).
|
|
| 2. |
- Abdulla, Parosh Aziz, 1961-, et al.
(author)
-
Flatten and Conquer : A Framework for Efficient Analysis of String Constraints
- 2017
-
In: SIGPLAN notices. - New York, NY, USA : ACM. - 0362-1340 .- 1558-1160. - 9781450349888 ; 52:6, s. 602-617, s. 602-617
-
Journal article (peer-reviewed)abstract
- We describe a uniform and efficient framework for checking the satisfiability of a large class of string constraints. The framework is based on the observation that both satisfiability and unsatisfiability of common constraints can be demonstrated through witnesses with simple patterns. These patterns are captured using flat automata each of which consists of a sequence of simple loops. We build a Counter-Example Guided Abstraction Refinement (CEGAR) framework which contains both an under-and an over-approximation module. The flow of information between the modules allows to increase the precision in an automatic manner. We have implemented the framework as a tool and performed extensive experimentation that demonstrates both the generality and efficiency of our method.
|
|
| 3. |
- Ahrendt, Wolfgang, 1967, et al.
(author)
-
Practical Aspects of Automated Deduction for Program Verification
- 2010
-
In: KI - Künstliche Intelligenz. - : Springer Science and Business Media LLC. - 0933-1875 .- 1610-1987. ; 24:1, s. 43-49
-
Journal article (peer-reviewed)abstract
- Software is vital for modern society. It is used in manysafety- or security-critical applications, where a high degree of correctness is desirable. Over the last years, technologies for the formal specification and verification of software -- using logic-based specification languages and automated deduction -- have matured and can be expected to complement and partly replace traditional software engineering methods in the future. Program verification is an increasingly important application area for automated deduction. The field has outgrown the area of academic case studies, and industry is showing serious interest. This article describes the aspects of automated deduction that are important for program verification in practice, and it gives an overview of the reasoning mechanisms, the methodology, and the architecture of modern program verification systems.
|
|
| 4. |
- Ahrendt, Wolfgang, 1967, et al.
(author)
-
TriCo—Triple Co-piloting of Implementation, Specification and Tests
- 2022
-
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 13701 LNCS, s. 174-187, s. 174-187
-
Conference paper (peer-reviewed)abstract
- This white paper presents the vision of a novel methodology for developing safety-critical software, which is inspired by late developments in learning based co-piloting of implementations. The methodology, called TriCo, integrates formal methods with learning based approaches to co-pilot the agile, simultaneous development of three artefacts: implementation, specification, and tests. Whenever the user changes any of these, a TriCo empowered IDE would suggest changes to the other two artefacts in such a way that the three are kept consistent. The user has the final word on whether the changes are accepted, rejected, or modified. In the latter case, consistency will be checked again and re-established. We discuss the emerging trends which put the community in a good position to realise this vision, describe the methodology and workflow, as well as challenges and possible solutions for the realisation of TriCo.
|
|
| 5. |
- Ahrendt, Wolfgang, 1967, et al.
(author)
-
Verifying Object-Oriented Programs with KeY: A Tutorial
- 2007
-
In: Formal Methods for Components and Objects, eds. de Boer, Bonsangue, Graf, de Roever. - 9783540747918 ; LNCS 4709
-
Conference paper (peer-reviewed)abstract
- This paper is a tutorial on performing formal specification and semi-automatic verification of Java programs with the formal software development tool KeY. This tutorial aims to fill the gap between elementary introductions using toy examples and state-of-art case studies by going through a self-contained, yet non-trivial, example. It is hoped that this contributes to explain the problems encountered in verification of imperative, object-oriented programs to a readership outside the limited community of active researchers.
|
|
| 6. |
|
|
| 7. |
- Amilon, Jesper, et al.
(author)
-
Automatic Program Instrumentation for Automatic Verification
- 2023
-
In: Computer Aided Verification. - Cham : Springer Nature. ; , s. 281-304, s. 281-304
-
Conference paper (peer-reviewed)abstract
- In deductive verification and software model checking, dealing with certain specification language constructs can be problematic when the back-end solver is not sufficiently powerful or lacks the required theories. One way to deal with this is to transform, for verification purposes, the program to an equivalent one not using the problematic constructs, and to reason about its correctness instead. In this paper, we propose instrumentation as a unifying verification paradigm that subsumes various existing ad-hoc approaches, has a clear formal correctness criterion, can be applied automatically, and can transfer back witnesses and counterexamples. We illustrate our approach on the automated verification of programs that involve quantification and aggregation operations over arrays, such as the maximum value or sum of the elements in a given segment of the array, which are known to be difficult to reason about automatically. We implement our approach in the MonoCera tool, which is tailored to the verification of programs with aggregation, and evaluate it on example programs, including SV-COMP programs.
|
|
| 8. |
- Arlt, Stephan, et al.
(author)
-
The Gradual Verifier
- 2014
-
In: NASA Formal Methods. - Switzerland : Springer International Publishing. - 9783319061993 ; , s. 313-327
-
Conference paper (peer-reviewed)
|
|
| 9. |
- Backeman, Peter, et al.
(author)
-
Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction
- 2018
-
In: Formal Methods in Computer-Aided Design. - : IEEE. - 9780983567882 ; , s. 50-59
-
Conference paper (peer-reviewed)abstract
- The inference of program invariants over machine arithmetic, commonly called bit-vector arithmetic, is an important problem in verification. Techniques that have been successful for unbounded arithmetic, in particular Craig interpolation, have turned out to be difficult to generalise to machine arithmetic: existing bit-vector interpolation approaches are based either on eager translation from bit-vectors to unbounded arithmetic, resulting in complicated constraints that are hard to solve and interpolate, or on bit-blasting to propositional logic, in the process losing all arithmetic structure. We present a new approach to bitvector interpolation, as well as bit-vector quantifier elimination (QE), that works by lazy translation of bit-vector constraints to unbounded arithmetic. Laziness enables us to fully utilise the information available during proof search (implied by decisions and propagation) in the encoding, and this way produce constraints that can be handled relatively easily by existing interpolation and QE procedures for Presburger arithmetic. The lazy encoding is complemented with a set of native proof rules for bit-vector equations and non-linear (polynomial) constraints, this way minimising the number of cases a solver has to consider
|
|
| 10. |
- Backeman, Peter, et al.
(author)
-
Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
- 2021
-
In: Formal methods in system design. - : SPRINGER. - 0925-9856 .- 1572-8102. ; 57:2, s. 121-156
-
Journal article (peer-reviewed)abstract
- The inference of program invariants over machine arithmetic, commonly called bit-vector arithmetic, is an important problem in verification. Techniques that have been successful for unbounded arithmetic, in particular Craig interpolation, have turned out to be difficult to generalise to machine arithmetic: existing bit-vector interpolation approaches are based either on eager translation from bit-vectors to unbounded arithmetic, resulting in complicated constraints that are hard to solve and interpolate, or on bit-blasting to propositional logic, in the process losing all arithmetic structure. We present a new approach to bit-vector interpolation, as well as bit-vector quantifier elimination (QE), that works by lazy translation of bit-vector constraints to unbounded arithmetic. Laziness enables us to fully utilise the information available during proof search (implied by decisions and propagation) in the encoding, and this way produce constraints that can be handled relatively easily by existing interpolation and QE procedures for Presburger arithmetic. The lazy encoding is complemented with a set of native proof rules for bit-vector equations and non-linear (polynomial) constraints, this way minimising the number of cases a solver has to consider. We also incorporate a method for handling concatenations and extractions of bit-vector efficiently.
|
|
