| 1. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
TriCo—Triple Co-piloting of Implementation, Specification and Tests
- 2022
-
Ingår i: 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
-
Konferensbidrag (refereegranskat)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.
|
|
| 2. |
- Alshnakat, Anoud, et al.
(författare)
-
Constraint-Based Contract Inference for Deductive Verification
- 2020
-
Ingår i: Deductive Software Verification. - Cham : Springer Nature. ; , s. 149-176
-
Bokkapitel (refereegranskat)abstract
- Assertion-based software model checking refers to techniques that take a program annotated with logical assertions and statically verify that the assertions hold whenever program execution is at the corresponding control point. While the associated annotation overhead is relatively low, these techniques are typically monolithic in that they explore the state space of the whole program at once, and may therefore scale poorly to large programs. Deductive software verification, on the other hand, refers to techniques that prove the correctness of a piece of software against a detailed specification of what it is supposed to accomplish or compute. The associated verification techniques are modular and scale well to large code bases, but incur an annotation overhead that is often very high, which is a real obstacle for deductive verification to be adopted in industry on a wider scale. In this paper we explore synergies between the two mentioned paradigms, and in particular, investigate how interpolation-based Horn solvers used for software model checking can be instrumented to infer missing procedure contracts for use in deductive verification, thus aiding the programmer in the code annotation process. We summarise the main developments in the area of automated contract inference, and present our own experiments with contract inference for C programs, based on solving Horn clauses. To drive the inference process, we put program assertions in the main function, and adapt our TriCera tool, a model checker based on the Horn solver Eldarica, to infer candidate contracts for all other functions. The contracts are output in the ANSI C Specification Language (ACSL) format, and are then validated with the Frama-C deductive verification tool for C programs.
|
|
| 3. |
|
|
| 4. |
- Amilon, Jesper, et al.
(författare)
-
Automatic Program Instrumentation for Automatic Verification
- 2023
-
Ingår i: Computer Aided Verification. - Cham : Springer Nature. ; , s. 281-304, s. 281-304
-
Konferensbidrag (refereegranskat)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. |
- Amilon, Jesper, et al.
(författare)
-
Deductive Verification Based Abstraction for Software Model Checking
- 2022
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer Nature. ; , s. 7-28
-
Konferensbidrag (refereegranskat)abstract
- The research community working on formal software verification has historically evolved into two main camps, grouped around two verification methods that are typically referred to as Deductive Verification and Model Checking. In this paper, we present an approach that applies deductive verification to formally justify abstract models for model checking in the TLA framework. We present a proof-of-concept tool chain for C programs, based on Frama-C for deductive verification and TLA+ for model checking. As a theoretical foundation, we summarise a previously developed abstract contract theory as a framework for combining these two methods. Since the contract theory adheres to the principles of contract based design, this justifies the use of the approach in a real-world system design setting. We evaluate our approach on two case studies: a simple C program simulating opening and closing of files, as well as a C program based on real software from the automotive industry.
|
|
| 6. |
- Bubel, Richard, et al.
(författare)
-
Trace-based Deductive Verification
- 2023
-
Ingår i: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning. - : EasyChair. ; , s. 73-95
-
Konferensbidrag (refereegranskat)abstract
- Contracts specifying a procedure’s behavior in terms of pre- and postconditions are essential for scalable software verification, but cannot express any constraints on the events occurring during execution of the procedure. This necessitates to annotate code with intermediate assertions, preventing full specification abstraction. We propose a logic over symbolic traces able to specify recursive procedures in a modular manner that refers to specified programs only in terms of events. We also provide a deduction system based on symbolic execution and induction that we prove to be sound relative to a trace semantics. Our work generalizes contract-based to trace-based deductive verification by extending the notion of state-based contracts to trace-based contracts.
|
|
| 7. |
- de C. Gomes, Pedro, et al.
(författare)
-
Specification and verification of synchronization with condition variables
- 2018
-
Ingår i: Science of Computer Programming. - : Elsevier. - 0167-6423 .- 1872-7964. ; 163, s. 174-189
-
Tidskriftsartikel (refereegranskat)abstract
- This paper proposes a technique to specify and verify the correct synchronization of concurrent programs with condition variables. We define correctness of synchronization as the liveness property: “every thread synchronizing under a set of condition variables eventually exits the synchronization block”, under the assumption that every such thread eventually reaches its synchronization block. Our technique does not avoid the combinatorial explosion of interleavings of thread behaviours. Instead, we alleviate it by abstracting away all details that are irrelevant to the synchronization behaviour of the program, which is typically significantly smaller than its overall behaviour. First, we introduce SyncTask, a simple imperative language to specify parallel computations that synchronize via condition variables. We consider a SyncTask program to have a correct synchronization iff it terminates. Further, to relieve the programmer from the burden of providing specifications in SyncTask, we introduce an economic annotation scheme for Java programs to assist the automated extraction of SyncTask programs capturing the synchronization behaviour of the underlying program. We show that every Java program annotated according to the scheme (and satisfying the assumption mentioned above) has a correct synchronization iff its corresponding SyncTask program terminates. We then show how to transform the verification of termination of the SyncTask program into a standard reachability problem over Coloured Petri Nets that is efficiently solvable by existing Petri Net analysis tools. Both the SyncTask program extraction and the generation of Petri Nets are implemented in our STAVE tool. We evaluate the proposed framework on a number of test cases.
|
|
| 8. |
- De Carvalho Gomes, Pedro, et al.
(författare)
-
Specification and verification of synchronization with condition variables
- 2017
-
Ingår i: 5th International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2016. - Cham : Springer. - 9783319539454 ; , s. 3-19
-
Konferensbidrag (refereegranskat)abstract
- In this paper we propose a technique to specify and verify the correct synchronization of concurrent programs with condition variables. We define correctness as the liveness property: “every thread synchronizing under a set of condition variables eventually exits the synchronization”, under the assumption that every such thread eventually reaches its synchronization block. Our technique does not avoid the combinatorial explosion of interleavings of thread behaviors. Instead, we alleviate it by abstracting away all details that are irrelevant to the synchronization behavior of the program, which is typically significantly smaller than its overall behavior. First, we introduce SyncTask, a simple imperative language to specify parallel computations that synchronize via condition variables. We consider a SyncTask program to have a correct synchronization iff it terminates. Further, to relieve the programmer from the burden of providing specifications in SyncTask, we introduce an economic annotation scheme for Java programs to assist the automated extraction of SyncTask programs capturing the synchronization behavior of the underlying program. We prove that every Java program annotated according to the scheme (and satisfying the assumption) has a correct synchronization iff its corresponding SyncTask program terminates. We show how to transform the verification of termination into a standard reachability problem over Colored Petri Nets that is efficiently solvable by existing Petri Net analysis tools. Both the SyncTask program extraction and the generation of Petri Nets are implemented in our STaVe tool. We evaluate the proposed framework on a number of test cases as a proof-of-concept.
|
|
| 9. |
- Eshghie, Mojtaba, et al.
(författare)
-
Dynamic Vulnerability Detection on Smart Contracts Using Machine Learning
- 2021
-
Ingår i: Proceedings Of Evaluation And Assessment In Software Engineering (EASE 2021). - New York, NY, USA : Association for Computing Machinery (ACM). ; , s. 305-312
-
Konferensbidrag (refereegranskat)abstract
- In this work we propose Dynamit, a monitoring framework to detect reentrancy vulnerabilities in Ethereum smart contracts. The novelty of our framework is that it relies only on transaction metadata and balance data from the blockchain system; our approach requires no domain knowledge, code instrumentation, or special execution environment. Dynamit extracts features from transaction data and uses a machine learning model to classify transactions as benign or harmful. Therefore, not only can we find the contracts that are vulnerable to reentrancy attacks, but we also get an execution trace that reproduces the attack. Using a random forest classifier, our model achieved more than 90 percent accuracy on 105 transactions, showing the potential of our technique.
|
|
| 10. |
- Felderer, Michael, 1978-, et al.
(författare)
-
Formal methods in industrial practice - Bridging the gap (track summary)
- 2018
-
Ingår i: Lect. Notes Comput. Sci.. - Cham : Springer Verlag. - 9783030034269 ; , s. 77-81
-
Konferensbidrag (refereegranskat)abstract
- Already for many decades, formal methods are considered to be the way forward to help the software industry to make more reliable and trustworthy software. However, despite this strong belief, and many individual success stories, no real change in industrial software development seems to happen. In fact, the software industry is moving fast forward itself, and the gap between what formal methods can achieve, and the daily software development practice does not seem to get smaller (and might even be growing).
|
|
