4 papers
Contract Based Verification of Non-functional Requirements for Embedded Automotive C Code
Jesper Amilon, Merlijn Sevenhuijsen, Mattias Nyberg +1
Code contracts provide a robust way to specify functional requirements of safety-critical software in embedded systems. For example, the ANSI/ISO C Specification Language (ACSL) ca…
Contract Based Program Models for Software Model Checking
Jesper Amilon, Dilian Gurov
Model checking temporal properties of software is algorithmically hard. To be practically feasible, it usually requires the creation of simpler, abstract models of the software, ov…
AutoDeduct: A Tool for Automated Deductive Verification of C Code
Jesper Amilon, Dilian Gurov, Christian Lidström +3
Deductive verification has become a mature paradigm for the verification of industrial software. Applying deductive verification, however, requires that every function in the code…
A Program Instrumentation Framework for Automatic Verification
Jesper Amilon, Zafer Esen, Dilian Gurov +3
In deductive verification and software model checking, dealing with certain specification language constructs can be problematic when the back-end solver is not sufficiently powerf…