Validation, Synthesis and Optimization for Cyber-Physical Systems
Abstract elided by the publisher.
26,098 papers · page 489 of 1,305
FlyFast: A Mean Field Model Checker
Abstract elided by the publisher.
HipTNT+: A Termination and Non-termination Analyzer by Second-Order Abduction - (Competition Contribution)
Abstract elided by the publisher.
Fair Termination for Parameterized Probabilistic Concurrent Systems
We consider the problem of automatically verifying that a parameterized family of probabilistic concurrent systems terminates with probability one for all instances against adversarial schedulers. A parameterized family defines an infinite-state system: for each number n, the fam…
A Novel Learning Algorithm for Büchi Automata Based on Family of DFAs and Classification Trees
In this paper, we propose a novel algorithm to learn a Buchi automaton from a teacher who knows an \(\omega \)-regular language. The algorithm is based on learning a formalism named family of DFAs (FDFAs) recently proposed by Angluin and Fisman [10]. The main catch is that we use…
ARES: Adaptive Receding-Horizon Synthesis of Optimal Plans
We introduce ARES, an efficient approximation algorithm for generating optimal plans action sequences that take an initial state of a Markov Decision Process MDP to a state whose cost is below a specified convergence threshold. ARES uses Particle Swarm Optimization, with adaptive…
Optimizing and Caching SMT Queries in SymDIVINE - (Competition Contribution)
Abstract elided by the publisher.
Lazy-CSeq 2.0: Combining Lazy Sequentialization with Abstract Interpretation - (Competition Contribution)
Abstract elided by the publisher.
Connecting Program Synthesis and Reachability: Automatic Program Repair Using Test-Input Generation
We prove that certain formulations of program synthesis and reachability are equivalent. Specifically, our constructive proof shows the reductions between the template-based synthesis problem, which generates a program in a pre-specified form, and the reachability problem, which …
Automatic Verification of Finite Precision Implementations of Linear Controllers
Abstract elided by the publisher.
Counterexample-Guided Model Synthesis
Abstract elided by the publisher.
DepthK: A k-Induction Verifier Based on Invariant Inference for C Programs - (Competition Contribution)
Abstract elided by the publisher.
HARE: A Hybrid Abstraction Refinement Engine for Verifying Non-linear Hybrid Automata
Abstract elided by the publisher.
CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs
Abstract elided by the publisher.
An Abstraction Technique for Parameterized Model Checking of Leader Election Protocols: Application to FTSP
Abstract elided by the publisher.
On Optimization Modulo Theories, MaxSMT and Sorting Networks
Optimization Modulo Theories $$\text {OMT}$$ is an extension of SMT which allows for finding models that optimize given objectives. Partial weighted MaxSMT---or equivalently $$\text {OMT}$$ with Pseudo-Boolean objective functions, $$\text {OMT+PB}$$ --- is a very-relevant strict …
Discriminating Traces with Time
What properties about the internals of a program explain the possible differences in its overall running time for different inputs? In this paper, we propose a formal framework for considering this question we dub trace-set discrimination. We show that even though the algorithmic…
HQSpre - An Effective Preprocessor for QBF and DQBF
Abstract elided by the publisher.
Static Detection of DoS Vulnerabilities in Programs that Use Regular Expressions
In an algorithmic complexity attack, a malicious party takes advantage of the worst-case behavior of an algorithm to cause denial-of-service. A prominent algorithmic complexity attack is regular expression denial-of-service (ReDoS), in which the attacker exploits a vulnerable reg…
Partitioned Memory Models for Program Analysis
Abstract elided by the publisher.