5 papers
A proof-carrying architecture for synthetic genetic logic circuits under stochastic temporal contracts
Arman Ferdowsi, Laura Kovacs
Genetic design automation maps Boolean specifications to regulatory networks and DNA sequences, but a successful mapping does not establish the probability that every output remain…
Completeness of Synthesis under Realizability Assumptions using Superposition
Márton Hajdu, Petra Hozzová, Laura Kovács +1
Program synthesis is the task of automatically deriving a program that has been specified by a user in advance. Combining automated theorem proving with program synthesis enables t…
Certificate-Aware Property-Directed Reachability
Arman Ferdowsi, Laura Kovacs
Property-Directed Reachability (PDR/IC3) is widely used for hardware safety verification. Most implementations optimize time-to-answer, but certified workflows also require compact…
A Neurosymbolic Approach to Loop Invariant Generation via Weakest Precondition Reasoning
Daragh King, Vasileios Koutavas, Laura Kovacs
Loop invariant generation remains a critical bottleneck in automated program verification. Recent work has begun to explore the use of Large Language Models (LLMs) in this area, ye…
LLMs and Fuzzing in Tandem: A New Approach to Automatically Generating Weakest Preconditions
Daragh King, Vasileios Koutavas, Laura Kovacs
The weakest precondition (WP) of a program describes the largest set of initial states from which all terminating executions of the program satisfy a given postcondition. The gener…