More Like this

1. Comprehensive Memory Safety Validation: An Alternative Approach to Memory Safety

   https://doi.org/10.1109/MSEC.2024.3379947  

   Huang, Kaiming; Payer, Mathias; Qian, Zhiyun; Sampson, Jack; Tan, Gang; Jaeger, Trent (July 2024, IEEE Security & Privacy)
2. Safety and Co-safety Comparator Automata for Discounted-Sum Inclusion

   https://doi.org/10.1007/978-3-030-25540-4_4  

   Bansal, Suguman (July 2019, Computer-Aided Verification)

   Discounted-sum inclusion (DS-inclusion, in short) formalizes the goal of comparing quantitative dimensions of systems such as cost, resource consumption, and the like, when the mode of aggregation for the quantitative dimension is discounted-sum aggregation. Discounted-sum comparator automata, or DS-comparators in short, are Buechi automata that read two in nite sequences of weights synchronously and relate their discounted-sum. Recent empirical investigations have shown that while DS-comparators enable competitive algorithms for DS-inclusion, they still suffer from the scalability bottleneck of Bueuchi operations. Motivated by the connections between discounted-sum and Buechi automata, this paper undertakes an investigation of language-theoretic properties of DS-comparators in order to mitigate the challenges of Buechi DS-comparators to achieve improved scalability of DS-inclusion. Our investigation uncovers that DS-comparators possess safety and co-safety language-theoretic properties. As a result, they enable reductions based on subset construction-based methods as opposed to higher complexity Buechi complementation, yielding tighter worst-case complexity and improved empirical scalability for DS-inclusion. 

   more » « less
3. BOGO: Buy Spatial Memory Safety, Get Temporal Memory Safety (Almost) Free

   https://doi.org/10.1145/3297858.3304017  

   Zhang, Tong; Lee, Dongyoon; Jung, Changhee (April 2019, Proceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems)
4. Safety-Aware Apprenticeship Learning

   Zhou, Weichao; Li, Wenchao (January 2018, Computer-Aided Verification)
5. Compositional Safety LTL Synthesis

   Bansal, S; De Giacomo, G; Di Stasio, A; Li, Y; Vardi, MY; Zhu, S. (February 2023, Verified Software. Theories, Tools and Experiments.. VSTTE 2022)

   Lal, A; Tonetta, S. (Ed.)

   Reactive synthesis holds the promise of generating automatically a verifiably correct program from a high-level specification. A popular such specification language is Linear Temporal Logic (LTL). Unfortunately, synthesizing programs from general LTL formulas, which relies on first constructing a game arena and then solving the game, does not scale to large instances. The specifications from practical applications are usually large conjunctions of smaller LTL formulas, which inspires existing compositional synthesis approaches to take advantage of this structural information. The main challenge here is that they solve the game only after obtaining the game arena, the most computationally expensive part in the procedure. In this work, we propose a compositional synthesis technique to tackle this difficulty by synthesizing a program for each small conjunct separately and composing them one by one. While this approach does not work for general LTL formulas, we show here that it does work for Safety LTL formulas, a popular and important fragment of LTL. While we have to compose all the programs of small conjuncts in the worst case, we can prune the intermediate programs to make later compositions easier and immediately conclude unrealizable as soon as some part of the specification is found unrealizable. By comparing our compositional approach with a portfolio of all other approaches, we observed that our approach was able to solve a notable number of instances not solved by others. In particular, experiments on scalable conjunctive benchmarks showed that our approach scale well and significantly outperform current Safety LTL synthesis techniques. We conclude that our compositional approach is an important contribution to the algorithmic portfolio of Safety LTL synthesis. 

   more » « less