Model Checking Software

Automated Consistency Analysis for Legal Contracts.- Monitoring Cyber-Physical Systems using a Tiny Twin to Prevent Cyber-Attacks.- Synthesis of Rigorous Floating-Point Predicates.- Statistical Model Checking for Probabilistic Hyperproperties of Real-Valued Signals.- SpecRepair: Counter-Example Guided Safety Repair of Deep Neural Networks.- Verifying the SHA-3 Implementation from OpenSSL with the Software Analysis Workbench.- Bounded-Memory Runtime Enforcement.- Solving String Theories involving Regular Membership Predicates using SAT.