| 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. |
- 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.
|
|
| 3. |
|
|
| 4. |
- 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.
|
|
| 5. |
- 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.
|
|
| 6. |
- Chen, Taolue, et al.
(author)
-
A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type
- 2020
-
In: ATVA 2020. - Cham : Springer Nature. - 9783030591519 - 9783030591526 ; , s. 325-342
-
Conference paper (peer-reviewed)abstract
- In this paper, we propose a decision procedure for a class of string-manipulating programs which includes not only a wide range of string operations such as concatenation, replaceAll, reverse, and finite transducers, but also those involving the integer data-type such as length, indexof, and substring. To the best of our knowledge, this represents one of the most expressive string constraint languages that is currently known to be decidable. Our decision procedure is based on a variant of cost register automata. We implement the decision procedure, giving rise to a new solver OSTRICH+. We evaluate the performance of OSTRICH+ on a wide range of existing and new benchmarks. The experimental results show that OSTRICH+ is the first string decision procedure capable of tackling finite transducers and integer constraints, whilst its overall performance is comparable with the state-of-the-art string constraint solvers.
|
|
| 7. |
- Chen, Taolue, et al.
(author)
-
Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables
- 2022
-
In: Proceedings of the ACM on Programming Languages. - : Association for Computing Machinery (ACM). - 2475-1421. ; 6
-
Journal article (peer-reviewed)abstract
- Regular expressions are a classical concept in formal language theory. Regular expressions in programming languages (RegEx) such as JavaScript, feature non-standard semantics of operators (e.g. greedy/lazy Kleene star), as well as additional features such as capturing groups and references. While symbolic execution of programs containing RegExes appeals to string solvers natively supporting important features of RegEx, such a string solver is hitherto missing. In this paper, we propose the first string theory and string solver that natively provides such support. The key idea of our string solver is to introduce a new automata model, called prioritized streaming string transducers (PSST), to formalize the semantics of RegEx-dependent string functions. PSSTs combine priorities, which have previously been introduced in prioritized finite-state automata to capture greedy/lazy semantics, with string variables as in streaming string transducers to model capturing groups. We validate the consistency of the formal semantics with the actual JavaScript semantics by extensive experiments. Furthermore, to solve the string constraints, we show that PSSTs enjoy nice closure and algorithmic properties, in particular, the regularity-preserving property (i.e., pre-images of regular constraints under PSSTs are regular), and introduce a sound sequent calculus that exploits these properties and performs propagation of regular constraints by means of taking post-images or pre-images. Although the satisfiability of the string constraint language is generally undecidable, we show that our approach is complete for the so-called straightline fragment. We evaluate the performance of our string solver on over 195 000 string constraints generated from an open-source RegEx library. The experimental results show the efficacy of our approach, drastically improving the existing methods (via symbolic execution) in both precision and efficiency.
|
|
| 8. |
- Chen, Yu-Fang, et al.
(author)
-
A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification)
- 2023
-
In: AUTOMATED DEDUCTION, CADE 29. - : Springer Nature. - 9783031384998 - 9783031384981 ; , s. 170-189
-
Conference paper (peer-reviewed)abstract
- We present a theory of Cartesian arrays, which are multi-dimensional arrays with support for the projection of arrays to subarrays, as well as for updating sub-arrays. The resulting logic is an extension of Combinatorial Array Logic (CAL) and is motivated by the analysis of quantum circuits: using projection, we can succinctly encode the semantics of quantum gates as quantifier-free formulas and verify the end-to-end correctness of quantum circuits. Since the logic is expressive enough to represent quantum circuits succinctly, it necessarily has a high complexity; as we show, it suffices to encode the k-color problem of a graph under a succinct circuit representation, an NEXPTIME-complete problem. We present an NEXPTIME decision procedure for the logic and report on preliminary experiments with the analysis of quantum circuits using this decision procedure.
|
|
| 9. |
- El Yaacoub, Ahmed, 1996-, et al.
(author)
-
NeRTA : Enabling Dynamic Software Updates in Mobile Robotics
- 2022
-
Conference paper (peer-reviewed)abstract
- We present NeRTA (Next Release Time Analysis), a technique to schedule dynamic software updates of the low-level control loops of mobile robots. Dynamic software updates enable software correction and evolution during system operation. In mobile robotics, they are crucial to resolve software defects without interrupting system operation or to enable on-the-fly extensions. Low-level control loops of mobile robots, however, are time sensitive and run on resource-constrained hardware with no operating system support. To minimize the impact of the update process, NeRTA safely schedules updates during times when the computing unit would otherwise be idle. It does so by utilizing information from the existing scheduling algorithm without impacting its operation. As such, NeRTA works orthogonal to the existing scheduler, retaining the existing platform-specific optimizations and fine-tuning, and may simply operate as a plug-in component. Our experimental evaluation shows that NeRTA estimates are within 15% of the actual idle times in more than three-quarters of the cases. We also show that the processing overhead of NeRTA is essentially negligible.
|
|
| 10. |
- El Yaacoub, Ahmed, et al.
(author)
-
Poster Abstract: Scheduling Dynamic Software Updates in Safety-critical Embedded Systems : the Case of Aerial Drones
- 2022
-
In: 2022 ACM/IEEE 13th International Conference on Cyber-Physical Systems (ICCPS). - : Institute of Electrical and Electronics Engineers (IEEE). - 9781665409674 - 9781665409681 ; , s. 284-285
-
Conference paper (peer-reviewed)abstract
- Dynamic software updates enable software evolution and bug fixes to embedded systems without disrupting their run-time operation. Scheduling dynamic updates for safety-critical embedded systems, such as aerial drones, must be done with great care. Otherwise, the system's control loop will be delayed leading to a partial or even complete loss of control, ultimately impacting the dependable operation. We propose an update scheduling algorithm called NeRTA, which schedules updates during the short times when the processor would have been idle. NeRTA consequently avoids the loss of control that would occur if an update delayed the execution of the control loop. The algorithm computes conservative estimations of idle times to determine if an update is possible, but is also sufficiently accurate that the estimated idle time is typically within 15% of the actual idle time.
|
|
