173 citations · 655 across the 66 of their papers we have counts for
7 papers · 1 filter
Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants
Alessandro Abate, Iury Bessa, Dario Cattaruzza +4
Modern control is implemented with digital microcontrollers, embedded within a dynamical plant that represents physical components. We present a new algorithm based on counter-exam…
Verification of the Tree-Based Hierarchical Read-Copy Update in the Linux Kernel
Lihao Liang, Paul E. McKenney, Daniel Kroening +1
Read-Copy Update (RCU) is a scalable, high-performance Linux-kernel synchronization mechanism that runs low-overhead readers concurrently with updaters. Production-quality RCU impl…
Equivalence Checking a Floating-point Unit against a High-level C Model (Extended Version)
Rajdeep Mukherjee, Saurabh Joshi, Andreas Griesmayer +2
Semiconductor companies have increasingly adopted a methodology that starts with a system-level design specification in C/C++/SystemC. This model is extensively simulated to ensure…
Satisfiability Checking meets Symbolic Computation (Project Paper)
E. Abraham, J. Abbott, B. Becker +12
Symbolic Computation and Satisfiability Checking are two research areas, both having their individual scientific focus but sharing also common interests in the development, impleme…
Satisfiability Checking and Symbolic Computation
E. Abraham, J. Abbott, B. Becker +12
Symbolic Computation and Satisfiability Checking are viewed as individual research areas, but they share common interests in the development, implementation and application of deci…
Sound Static Deadlock Analysis for C/Pthreads (Extended Version)
Daniel Kroening, Daniel Poetzl, Peter Schrammel +1
We present a static deadlock analysis approach for C/pthreads. The design of our method has been guided by the requirement to analyse real-world code. Our approach is sound (i.e.,…