4 citations · 12 across the 7 of their papers we have counts for
7 papers
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…
The Right Kind of Non-Determinism: Using Concurrency to Verify C Programs with Underspecified Semantics
Eduard Kamburjan, Nathan Wasser
We present a novel and well automatable approach to formal verification of C programs with underspecified semantics, i.e., a language semantics that leaves open the order of certai…
Deductive Verification of Programs with Underspecified Semantics by Model Extraction
Eduard Kamburjan, Nathan Wasser
We present a novel and well automatable approach to formal verification of programs with underspecified semantics, i.e., a language semantics that leaves open the order of certain…
Crowbar: Behavioral Symbolic Execution for Deductive Verification of Active Objects
Eduard Kamburjan, Marco Scaletta, Nils Rollshausen
We present the Crowbar tool, a deductive verification system for the ABS language. ABS models distributed systems with the Active Object concurrency model. Crowbar implements behav…
Tool Support for Validation of Formal System Models: Interactive Visualization and Requirements Traceability
Eduard Kamburjan, Jonas Stromberg
Development processes in various engineering disciplines are incorporating formal models to ensure safety properties of critical systems. The use of these formal models requires to…
Behavioral Program Logic and LAGC Semantics without Continuations (Technical Report)
Eduard Kamburjan
We present Behavioral Program Logic (BPL), a dynamic logic for trace properties that incorporates concepts from behavioral types and allows reasoning about non-functional propertie…
Stateful Behavioral Types for ABS
Eduard Kamburjan, Tzu-Chun Chen
It is notoriously hard to correctly implement a multiparty protocol which involves asynchronous/concurrent interactions and the constraints on states of multiple participants. To a…