43 citations · 170 across the 19 of their papers we have counts for
4 papers · 1 filter
A Supervisory Control Algorithm Based on Property-Directed Reachability
Koen Claessen, Jonatan Kilhamn, Laura Kovács +1
We present an algorithm for synthesising a controller (supervisor) for a discrete event system (DES) based on the property-directed reachability (PDR) model checking algorithm. The…
Splitting Proofs for Interpolation
Bernhard Gleiss, Laura Kovacs, Martin Suda
We study interpolant extraction from local first-order refutations. We present a new theoretical perspective on interpolation based on clearly separating the condition on logical s…
Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences
Andreas Humenberger, Maximilian Jaroschek, Laura Kovács
Analyzing and reasoning about safety properties of software systems becomes an especially challenging task for programs with complex flow and, in particular, with loops or recursio…
Symbolic Computation and Automated Reasoning for Program Analysis
Laura Kovacs
This talk describes how a combination of symbolic computation techniques with first-order theorem proving can be used for solving some challenges of automating program analysis, in…