SAS 2021

22 papers

1. A Multilanguage Static Analysis of Python Programs with Native C Extensions · Raphaël Monat, Abdelraouf Ouadjaout, Antoine Miné
2. Accelerating Program Analyses in Datalog by Merging Library Facts · Yifan Chen, Chenyang Yang, Xin Zhang, Yingfei Xiong, Hao Tang, Xiaoyin Wang + 1 more
3. Automated Verification of the Parallel Bellman-Ford Algorithm · Mohsen Safari, Wytse Oortwijn, Marieke Huisman
4. Automatic Synthesis of Data-Flow Analyzers · Xuezheng Xu, Xudong Wang, Jingling Xue
5. Backward Symbolic Execution with Loop Folding · Marek Chalupa, Jan Strejcek
6. Compositional Verification of Smart Contracts Through Communication Abstraction · Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, Arie Gurfinkel
7. Data Abstraction: A General Framework to Handle Program Verification of Data Structures · Julien Braine, Laure Gonnord, David Monniaux
8. Disjunctive Interval Analysis · Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey
9. Exploiting Verified Neural Networks via Floating Point Numerical Error · Kai Jia, Martin C. Rinard
10. Fast and Efficient Bit-Level Precision Tuning · Assalé Adjé, Dorra Ben Khalifa, Matthieu Martel
11. Hash Consed Points-To Sets · Mohamad Barbar, Yulei Sui
12. Improving Thread-Modular Abstract Interpretation · Michael Schwarz, Simmo Saan, Helmut Seidl, Kalmer Apinis, Julian Erhard, Vesal Vojdani
13. Reduced Products of Abstract Domains for Fairness Certification of Neural Networks · Denis Mazzucato, Caterina Urban
14. Selective Context-Sensitivity for k-CFA with CFL-Reachability · Jingbo Lu, Dongjie He, Jingling Xue
15. Selectively-Amortized Resource Bounding · Tianhan Lu, Bor-Yuh Evan Chang, Ashutosh Trivedi
16. Static Analysis of Endian Portability by Abstract Interpretation · David Delmas, Abdelraouf Ouadjaout, Antoine Miné
17. Static Analysis of ReLU Neural Networks with Tropical Polyhedra · Eric Goubault, Sébastien Palumby, Sylvie Putot, Louis Rustenholz, Sriram Sankaranarayanan
18. Symbolic Automatic Relations and Their Applications to SMT and CHC Solving · Takumi Shimoda, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato
19. Thread-Modular Analysis of Release-Acquire Concurrency · Divyanjali Sharma, Subodh Sharma
20. Toward Neural-Network-Guided Program Synthesis and Verification · Naoki Kobayashi, Taro Sekiyama, Issei Sato, Hiroshi Unno
21. Verified Functional Programming of an Abstract Interpreter · Lucas Franceschino, David Pichardie, Jean-Pierre Talpin
22. Verifying Low-Dimensional Input Neural Networks via Input Quantization · Kai Jia, Martin C. Rinard