| 1. |
|
|
| 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. |
- Alshnakat, Anoud, et al.
(författare)
-
HOL4P4 : Semantics for a Verified Data Plane
- 2022
-
Ingår i: EuroP4 2022. - New York, NY, USA : Association for Computing Machinery (ACM). ; , s. 39-45
-
Konferensbidrag (refereegranskat)abstract
- We introduce a formal semantics of P4 for the HOL4 interactive theorem prover. We exploit properties of the language, like the absence of call by reference and the copy-in/copy-out mechanism, to define a heapless small-step semantics that is abstract enough to simplify verification, but that covers the main aspects of the language: interaction with the architecture via externs, table match, and parsers. Our formalization is written in the Ott metalanguage, which allows us to export definitions to multiple interactive theorem provers. The exported HOL4 semantics allows us to establish machine-checkable proofs regarding the semantics, properties of P4 programs, and soundness of analysis tools.
|
|
| 4. |
- Alshnakat, Anoud, et al.
(författare)
-
HOL4P4: Mechanized Small-Step Semantics for P4
- 2024
-
Ingår i: Proceedings of the ACM on Programming Languages. - : Association for Computing Machinery (ACM). - 2475-1421. ; 8:OOPSLA1
-
Tidskriftsartikel (refereegranskat)abstract
- We present the first semantics of the network data plane programming language P4 able to adequately capture all key features of P416, the most recent version of P4, including external functions (externs) and concurrency. These features are intimately related since, in P4, extern invocations are the only points at which one execution thread can affect another. Reflecting P4's lack of a general-purpose memory and the presence of multithreading the semantics is given in small-step style and eschews the use of a heap. In addition to the P4 language itself, we provide an architectural level semantics, which allows the composition of P4-programmed blocks, models end-to-end packet processing, and can take into account features such as arbitration and packet recirculation. A corresponding type system is provided with attendant progress, preservation, and type-soundness theorems. Semantics, type system, and meta-theory are formalized in the HOL4 theorem prover. From this formalization, we derive a HOL4 executable semantics that supports verified execution of programs with partially symbolic packets able to validate simple end-to-end program properties.
|
|
