39 citations · 236 across the 34 of their papers we have counts for
36 papers
LISA -- A Modern Proof System
Simon Guilloud, Sankalp Gambhir, Viktor Kunčak
We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof che…
Orthologic with Axioms
Simon Guilloud, Viktor Kuncak
We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verifi…
On Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time
Simon Guilloud, Viktor Kunčak
We present a quasilinear time algorithm to decide the word problem on a natural algebraic structures we call orthocomplemented bisemilattices, a subtheory of boolean algebra. We us…
NP Satisfiability for Arrays as Powers
Rodrigo Raya, Viktor Kunčak
We show that the satisfiability problem for the quantifier-free theory of product structures with the equicardinality relation is in NP. As an application, we extend the combinator…
Verifying a Realistic Mutable Hash Table
Samuel Chassot, Viktor Kunčak
In this work, we verify the mutable LongMap from the Scala standard library, a hash table using open addressing within a single array, using the Stainless program verifier. As a re…
Proving and Disproving Programs with Shared Mutable Data
Georg Schmid, Viktor Kunčak
We present a tool for verification of deterministic programs with shared mutable references against specifications such as assertions, preconditions, postconditions, and read/write…