2,069 papers · page 7 of 104
François Hublet, Leonardo Lima, David A. Basin, Srdan Krstic, Dmitriy Traytel
Abstract Runtime enforcers receive events from a system and output commands ensuring the system’s policy compliance. Proactive enforcers extend traditional (reactive) enforcers by emitting commands at any time, rather only as a response to system actions. However, proactive enfor…
Geonho Hwang, Wonyeol Lee, Yeachan Park, Sejun Park, Feras Saad
Abstract The classical universal approximation (UA) theorem for neural networks establishes mild conditions under which a feedforward neural network can approximate a continuous function f with arbitrary accuracy. A recent result shows that neural networks also enjoy a more gener…
Hongjian Jiang, Anthony W. Lin, Oliver Markgraf, Philipp Rümmer, Daniel Stan
Abstract We present $$\textsf{HornStr}$$ HornStr , the first solver for invariant synthesis for Regular Model Checking (RMC) with the specification provided in the SMT-LIB 2.6 theory of strings. It is well-known that invariant synthesis for RMC subsumes various important verifica…
Yusuke Kawamoto, Kentaro Kobayashi, Kohei Suenaga
Abstract Statistical methods have been widely misused and misinterpreted in various scientific fields, raising significant concerns about the integrity of scientific research. To mitigate this problem, we propose a tool-assisted method for formally specifying and automatically ve…
Bram Kohlen, Maximilian Schäffeler, Mohammad Abdulaziz, Arnd Hartmanns, Peter Lammich
Abstract We present an efficiently executable, formally verified implementation of interval iteration for MDPs. Our correctness proofs span the entire development from the high-level abstract semantics of MDPs to a low-level implementation in LLVM that is based on floating-point …
Faezeh Labbaf, Tomás Kolárik, Martin Blicha, Grigory Fedyukovich, Michael Wand, Natasha Sharygina
Abstract We present a novel logic-based concept called Space Explanations for classifying neural networks that gives provable guarantees of the behavior of the network in continuous areas of the input feature space. To automatically generate space explanations, we leverage a rang…
Yong Lai, Kuldeep S. Meel, Roland H. C. Yap
Abstract Knowledge compilation (KC) involves compiling propositional constraints into tractable target languages which in turn efficiently support multiple analyses or queries of the constraints. Solving these queries plays a crucial role in the synthesis and verification of hard…
Zhaoyu Li, Hangrui Bi, Jialiang Sun, Zenan Li, Kaiyu Yang, Xujie Si
Abstract We introduce , a unified and versatile Python-based formal system for representing and reasoning about plane geometry problems. designs a new formal language that faithfully encodes geometric information, including diagrams, and integrates two complementary components to…
Yong Li, Soumyajit Paul, Sven Schewe, Qiyi Tang
Abstract Good-for-Games (GfG) automata require that their nondeterminism can be resolved on-the-fly, while unambiguous automata guarantee that no word has more than one accepting run. These two mutually exclusive ways of restricted nondeterminism play their roles independently in…
Elaine Li, Felix Stutz, Thomas Wies, Damien Zufferey
Abstract We present Sprout , the first sound and complete implementability checker for symbolic multiparty protocols. Sprout supports protocols with dependent refinements on message values, loop memory, and multiparty communication with generalized, sender-driven choice. Sprout c…
Aliaume Lopez, Rafal Stefanski
Abstract We introduce a high-level language with Python-like syntax for string-to-string, polyregular, first-order definable transductions. This language features function calls, boolean variables, and nested for-loops. We devise and implement a complete decision procedure for th…
Zhengyang Lu, Po-Chun Chien, Nian-Ze Lee, Arie Gurfinkel, Vijay Ganesh
Abstract In recent years, a diverse variety of hardware model-checking tools and techniques that exhibit complementary strengths and distinct weaknesses have been proposed. This state of affairs naturally suggests the use of algorithm-selection techniques to select the right tool…
Andrew Luka, Yakir Vizel
Abstract Property Directed Reachability ( Pdr ), also known as IC3, is a state-of-the-art model checking algorithm widely used for verifying safety properties. While Pdr is effective in finding inductive invariants, its underlying proof system, Resolution, limits its ability to c…
Yun-Rong Luo, Aman Goel, Karem A. Sakallah
Abstract We introduce , a new procedure that employs the quantified symmetric minimization algorithm from [12] to systematically derive quantified formulas that precisely capture the onset of cutoff and saturation in distributed protocols. performs symmetry-aware forward reachabi…
Denis Mazzucato, Abdalrhman Mohamed, Juneyoung Lee, Clark W. Barrett, Jim Grundy, John Harrison, Corina S. Pasareanu
Abstract Many security- and performance-critical domains, such as cryptography, rely on low-level verification to minimize the trusted computing surface and allow code to be written directly in assembly. However, verifying assembly code against a realistic machine model is a chal…
Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett
Abstract Lean is an increasingly popular proof assistant based on dependent type theory. Despite its success, it still lacks important automation features present in more seasoned proof assistants, such as the Sledgehammer tactic in Isabelle/HOL. A key aspect of Sledgehammer is t…
Sergei Novozhilov, Mingqi Yang, Mingshuai Chen, Zhiyang Li, Jianwei Yin
Abstract This paper introduces k -d PCPs – the class of probabilistic counter programs with $$k \in \mathbb {N}$$ k ∈ N counter variables inducing possibly infinite-state Markov chains. We show that the universal (positive) almost-sure termination problem is undecidable for k -d …
Elizaveta Pertseva, Alex Ozdemir, Shankara Pailoor, Alp Bassa, Sorawee Porncharoenwase, Isil Dillig, Clark W. Barrett
Abstract This paper presents a new refutation procedure for multimodular systems of integer constraints that commonly arise when verifying cryptographic protocols. These systems, involving polynomial equalities and disequalities modulo different constants, are challenging for exi…
George Pîrlea, Vladimir Gladshtein, Elad Kinsbruner, Qiyuan Zhao, Ilya Sergey
Abstract We present , an open-source framework for automated and interactive verification of transition systems, aimed specifically at conducting machine-assisted proofs about concurrent and distributed algorithms. is implemented on top of the proof assistant. It allows one to de…
Francesco Pontiggia, Ezio Bartocci, Michele Chiari
Abstract We present , the first model checking tool for probabilistic Pushdown Automata (pPDA) supporting temporal logic specifications. provides a user-friendly probabilistic modeling language with recursion that automatically translates into Probabilistic Operator Precedence Au…