Symbolic Execution

Symbolic Partial-Order Execution for Testing Multi-Threaded Programs [CAV 2020 Version]

We describe a technique for systematic testing of multi-threaded programs. We combine Quasi-Optimal Partial-Order Reduction, a state-of-the-art technique that tackles path explosion due to interleaving non-determinism, with symbolic execution to …

Symbolic Partial-Order Execution for Testing Multi-Threaded Programs [Extended Version]

We describe a technique for systematic testing of multi-threaded programs. We combine Quasi-Optimal Partial-Order Reduction, a state-of-the-art technique that tackles path explosion due to interleaving non-determinism, with symbolic execution to …

Interoperability-Guided Testing of QUIC Implementations Using Symbolic Execution

The main reason for the standardization of network protocols, like QUIC, is to ensure interoperability between implementations, which poses a challenging task. Manual tests are currently used to test the different existing implementations for …

Symbolic Liveness Analysis of Real-World Software

Liveness violation bugs are notoriously hard to detect, especially due to the difficulty inherent in applying formal methods to real-world programs. We present a generic and practically useful liveness property which defines a program as being live …

Towards Benchmark Optimization by Automated Equivalence Detection

Especially in the case of Cyber-Physical Systems (CPSs), testbed validations and benchmarks, while necessary, incur significant setup and operation costs. Optimized benchmark sets reduce the number of tests that need to be performed, which ultimately …

Floating-Point Symbolic Execution: A Case Study in N-Version Programming

Symbolic execution is a well-known program analysis technique for testing software, which makes intensive use of constraint solvers. Recent support for floating-point constraint solving has made it feasible to support floating-point reasoning in …

SymPerf: Predicting Network Function Performance

The softwarization of networks provides a new degree of flexibility in network operation but its software components can result in unexpected runtime performance and erratic network behavior. This challenges the deployment of flexible software …