5 citations · 7 across the 13 of their papers we have counts for
5 papers · 1 filter
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…
An Expressive Trace Logic for Recursive Programs
Dilian Gurov, Reiner Hähnle
We present an expressive logic over trace formulas, based on binary state predicates, chop, and least fixed-points, for precise specification of programs with recursive procedures.…
A Hoare Logic for Domain Specification (Full Version)
Eduard Kamburjan, Dilian Gurov
Programs must be correct with respect to their application domain. Yet, the program specification and verification approaches so far only consider correctness in terms of computati…
Soundness and Completeness of a Model-Checking Proof System for CTL
Georg Friedrich Schuppe, Dilian Gurov
We propose a local model-checking proof system for a fragment of CTL. The rules of the proof system are motivated by the well-known fixed-point characterisation of CTL based on unf…
An Abstract Contract Theory for Programs with Procedures
Christian Lidström, Dilian Gurov
When developing complex software and systems, contracts provide a means for controlling the complexity by dividing the responsibilities among the components of the system in a hier…