CosySEL: Improving SAT Solving Using Local Symmetries
Abstract elided by the publisher.
642 papers · page 5 of 33
Compositional Verification of Stigmergic Collective Systems
Abstract elided by the publisher.
Sound Symbolic Execution via Abstract Interpretation and Its Application to Security
Symbolic execution is a program analysis technique commonly utilized to determine whether programs violate properties and, in case violations are found, to generate inputs that can trigger them. Used in the context of security properties such as noninterference, symbolic executio…
Synthesizing History and Prophecy Variables for Symbolic Model Checking
Abstract elided by the publisher.
Solving Constrained Horn Clauses over Algebraic Data Types
Abstract elided by the publisher.
ARENA: Enhancing Abstract Refinement for Neural Network Verification
Abstract elided by the publisher.
Relational String Abstract Domains
Abstract elided by the publisher.
Flavors of Sequential Information Flow
Abstract elided by the publisher.
Fanoos: Multi-resolution, Multi-strength, Interactive Explanations for Learned Systems
Machine learning becomes increasingly important to tune or even synthesize the behavior of safety-critical components in highly non-trivial environments, where the inability to understand learned components in general, and neural nets in particular, poses serious obstacles to the…
Loop Verification with Invariants and Contracts
Abstract elided by the publisher.
EPMC Gets Knowledge in Multi-agent Systems
Abstract elided by the publisher.
High Assurance Software for Financial Regulation and Business Platforms
Abstract elided by the publisher.
Gradient-Descent for Randomized Controllers Under Partial Observability
Randomization is a powerful technique to create robust controllers, in particular in partially observable settings. The degrees of randomization have a significant impact on the system performance, yet they are intricate to get right. The use of synthesis algorithms for parametri…
Automata-Driven Partial Order Reduction and Guided Search for LTL Model Checking
Abstract elided by the publisher.
Verifying Pufferfish Privacy in Hidden Markov Models
Pufferfish is a Bayesian privacy framework for designing and analyzing privacy mechanisms. It refines differential privacy, the current gold standard in data privacy, by allowing explicit prior knowledge in privacy analysis. Through these privacy frameworks, a number of privacy m…
A Flow-Insensitive-Complete Program Representation
International audience
Lightweight Shape Analysis Based on Physical Types
Abstract elided by the publisher.
Fast Three-Valued Abstract Bit-Vector Arithmetic
Abstract elided by the publisher.
Satisfiability and Synthesis Modulo Oracles
In classic program synthesis algorithms, such as counterexample-guided inductive synthesis (CEGIS), the algorithms alternate between a synthesis phase and an oracle (verification) phase. Many synthesis algorithms use a white-box oracle based on satisfiability modulo theory (SMT) …
Bisimulations for Neural Network Reduction
We present a notion of bisimulation that induces a reduced network which is semantically equivalent to the given neural network. We provide a minimization algorithm to construct the smallest bisimulation equivalent network. Reductions that construct bisimulation equivalent neural…