Wyniki wyszukiwania - BazTech

Ograniczanie wyników

2 Fundamenta Informaticae

2 2020

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: deductive verification

Sortuj według:

Ogranicz wyniki do:

Abstract Contract Synthesis and Verification in the Symbolic 𝕂 Framework

Alpuente Maria, Pardo Daniel, Villanueva Alicia

Fundamenta Informaticae

2020

Vol. 177, nr 3/4

235--273

In this article, we propose a symbolic technique that can be used for automatically inferring software contracts from programs that are written in a non-trivial fragment of C, called KERNEL C, that supports pointer-based structures and heap manipulation. Starting from the semantic definition of KERNEL C in the 𝕂 semantic framework, we enrich the symbolic execution facilities recently provided by 𝕂 with novel capabilities for contract synthesis that are based on abstract subsumption. Roughly speaking, we define an abstract symbolic technique that axiomatically explains the execution of any (modifier) C function by using other (observer) routines in the same program. We implemented our technique in the automated tool KIND SPEC 2.1, which generates logical axioms that express pre- and post-condition assertions which define the precise input/output behavior of the C routines. Thanks to the integrated support for symbolic execution and deductive verification provided by 𝕂, some synthesized axioms that cannot be guaranteed to be correct by construction due to abstraction can finally be verified in our setting with little effort.

A Constructor-Based Reachability Logic for Rewrite Theories

Skeirik Stephen, Stefanescu Andrei, Meseguer José

Fundamenta Informaticae

2020

Vol. 173, nr 4

315--382

Reachability logic has been applied to K rewrite-rule-based language definitions as a language-generic logic of programs to verify a wide range of sophisticated programs in conventional languages. Here we study how reachability logic can be made not just language-generic, but also rewrite-theory-generic, so that we can verify both conventional programs based on their rewriting logic operational semantics and distributed system designs specified as rewrite theories. A theory-generic reachability logic is presented and proved sound for a wide class of rewrite theories. Particular attention is given to increasing the logic's automation by means of constructor-based semantic unification, matching, narrowing, and satisfiability procedures. The relationships to Hoare logic and LTL are discussed, new methods for proving invariants of possibly never terminating distributed systems are developed, and experiments with a prototype implementation illustrating the new methods are presented.