Sumanth Prabhu
ABSTRACT
The problem of synthesizing specifications of undefined procedures has a broad range of applications, but the usefulness of the generated specifications depends on their quality. In this paper, we propose a technique for finding maximal and non-vacuous specifications. Maximality allows for more choices for implementations of undefined procedures, and non-vacuity ensures that safety assertions are reachable. To handle programs with complex control flow, our technique discovers not only specifications but also inductive invariants. Our iterative algorithm lazily generalizes non-vacuous specifications in a counterexample-guided loop. The key component of our technique is an effective non-vacuous specification synthesis algorithm. We have implemented the approach in a tool called HornSpec, taking as input systems of constrained Horn clauses. We have experimentally demonstrated the tool's effectiveness, efficiency, and the quality of generated specifications on a range of benchmarks.
- Aws Albarghouthi, Isil Dillig, and Arie Gurfinkel. 2016. Maximal specification synthesis. In POPL. ACM, 789–801. https://doi.org/10.1145/2914770.2837628 Google Scholar
Digital Library
- Rajeev Alur, Rastislav Bodík, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013. Syntax-Guided Synthesis. In FMCAD. IEEE, 1–17. https://doi.org/10.3233/978-1-61499-495-4-1 Google ScholarCross Ref
- Rajeev Alur, Pavol Cerný, P. Madhusudan, and Wonhong Nam. 2005. Synthesis of interface specifications for Java classes. In POPL. ACM, 98–109. https://doi.org/10.1145/1040305.1040314 Google ScholarDigital Library
- Rajeev Alur, Dana Fisman, Saswat Padhi, Andrew Reynolds, Rishabh Singh, and Abhishek Udupa. 2019. SyGuS-Comp 2019. https://sygus.org/comp/2019/results-slides.pdfGoogle Scholar
- Glenn Ammons, Rastislav Bodík, and James R. Larus. 2002. Mining specifications. In POPL. ACM, 4–16. https://doi.org/10.1145/503272.503275 Google ScholarDigital Library
- Ezio Bartocci, Dirk Beyer, Paul E. Black, Grigory Fedyukovich, Hubert Garavel, Arnd Hartmanns, Marieke Huisman, Fabrice Kordon, Julian Nagele, Mihaela Sighireanu, Bernhard Steffen, Martin Suda, Geoff Sutcliffe, Tjark Weber, and Akihisa Yamada. 2019. TOOLympics 2019: An Overview of Competitions in Formal Methods. In TACAS, Part III (LNCS, Vol. 11429). Springer, 3–24. https://doi.org/10.1007/978-3-030-17502-3_1 Google ScholarCross Ref
- Osbert Bastani, Saswat Anand, and Alex Aiken. 2015. Specification Inference Using Context-Free Language Reachability. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015. 553–566. https://doi.org/10.1145/2676726.2676977 Google ScholarDigital Library
- Nels E. Beckman and Aditya V. Nori. 2011. Probabilistic, modular and scalable inference of typestate specifications. In PLDI. ACM, 211–221. https://doi.org/10.1145/1993498.1993524 Google ScholarDigital Library
- Tewodros A. Beyene, Swarat Chaudhuri, Corneliu Popeea, and Andrey Rybalchenko. 2014. A constraint-based approach to solving games on infinite graphs. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014. 221–234. https://doi.org/10.1145/2535838.2535860 Google ScholarDigital Library
- Nikolaj Bjørner and Mikolás Janota. 2015. Playing with Quantified Satisfaction. In LPAR (short papers) (EPiC Series in Computing, Vol. 35). EasyChair, 15–27. https://easychair.org/publications/paper/jmMGoogle Scholar
- Cristiano Calcagno, Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. 2011. Compositional Shape Analysis by Means of Bi-Abduction. J. ACM, 58, 6 (2011), 26:1–26:66. https://doi.org/10.1145/2049697.2049700 Google ScholarDigital Library
- Adrien Champion, Tomoya Chiba, Naoki Kobayashi, and Ryosuke Sato. 2018. ICE-Based Refinement Type Discovery for Higher-Order Functional Programs. In TACAS, Part I (LNCS, Vol. 10805). Springer, 365–384. https://doi.org/10.1007/978-3-319-89960-2_20 Google ScholarCross Ref
- Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta. 2013. Parameter synthesis with IC3. In FMCAD. IEEE, 165–168. http://ieeexplore.ieee.org/document/6679406/Google Scholar
- Patrick Cousot, Radhia Cousot, Manuel Fähndrich, and Francesco Logozzo. 2013. Automatic Inference of Necessary Preconditions. In Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings. 128–148. https://doi.org/10.1007/978-3-642-35873-9_10 Google ScholarDigital Library
- Ankush Das, Shuvendu K. Lahiri, Akash Lal, and Yi Li. 2015. Angelic Verification: Precise Verification Modulo Unknowns. In CAV, Part I (LNCS, Vol. 9206). Springer, 324–342. https://doi.org/10.1007/978-3-319-21690-4_19 Google ScholarCross Ref
- Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In TACAS (LNCS, Vol. 4963). Springer, 337–340. https://doi.org/10.1007/978-3-540-78800-3_24 Google ScholarCross Ref
- Isil Dillig, Thomas Dillig, Boyang Li, and Kenneth L. McMillan. 2013. Inductive invariant generation via abductive inference. In OOPSLA. ACM, 443–456. https://doi.org/10.1145/2509136.2509511 Google ScholarDigital Library
- P. Ezudheen, Daniel Neider, Deepak D’Souza, Pranav Garg, and P. Madhusudan. 2018. Horn-ICE learning for synthesizing invariants and contracts. PACMPL, 2, OOPSLA (2018), 131:1–131:25. https://doi.org/10.1145/3276501 Google ScholarDigital Library
- Grigory Fedyukovich, Maaz Bin Safeer Ahmad, and Rastislav Bodík. 2017. Gradual Synthesis for Static Parallelization of Single-Pass Array-Processing Programs. In PLDI. ACM, 572–585. https://doi.org/10.1145/3062341.3062382 Google ScholarDigital Library
- Grigory Fedyukovich, Samuel Kaufman, and Rastislav Bodík. 2017. Sampling Invariants from Frequency Distributions. In FMCAD. IEEE, 100–107. https://doi.org/10.23919/FMCAD.2017.8102247 Google ScholarCross Ref
- Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar, and Aarti Gupta. 2018. Solving Constrained Horn Clauses Using Syntax and Data. In FMCAD. IEEE, 170–178. https://doi.org/10.23919/FMCAD.2018.8603011 Google ScholarCross Ref
- Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar, and Aarti Gupta. 2019. Quantified Invariants via Syntax-Guided Synthesis. In CAV, Part I (LNCS, Vol. 11561). Springer, 259–277. https://doi.org/10.1007/978-3-030-25540-4_14 Google ScholarCross Ref
- Grigory Fedyukovich, Philipp Rümmer, and Arie Gurfinkel. 2019. CHC-COMP. https://chc-comp.github.io/2019/chc-comp19.pdfGoogle Scholar
- Cormac Flanagan and K. Rustan M. Leino. 2001. Houdini: an Annotation Assistant for ESC/Java. In FME (LNCS, Vol. 2021). Springer, 500–517. https://doi.org/10.1007/3-540-45251-6_29 Google ScholarCross Ref
- Pierre-Loïc Garoche, Temesghen Kahsai, and Xavier Thirioux. 2016. Hierarchical State Machines as Modular Horn Clauses. In HCVS (EPTCS, Vol. 219). 15–28. https://doi.org/10.4204/EPTCS.219.2 Google ScholarCross Ref
- Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar. 2018. Online detection of effectively callback free objects with applications to smart contracts. PACMPL, 2, POPL (2018), 48:1–48:28. https://doi.org/10.1145/3158136 Google ScholarDigital Library
- Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. 2015. The SeaHorn Verification Framework. In CAV (LNCS, Vol. 9206). Springer, 343–361. https://doi.org/10.1007/978-3-319-21690-4_20 Google ScholarCross Ref
- Kodai Hashimoto and Hiroshi Unno. 2015. Refinement Type Inference via Horn Constraint Optimization. In SAS, Sandrine Blazy and Thomas P. Jensen (Eds.) (LNCS, Vol. 9291). Springer, 199–216. https://doi.org/10.1007/978-3-662-48288-9_12 Google ScholarCross Ref
- Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. 2005. Permissive interfaces. In ESEC/SIGSOFT FSE. ACM, 31–40. https://doi.org/10.1145/1081706.1081713 Google ScholarDigital Library
- Hossein Hojjat, Filip Konecný, Florent Garnier, Radu Iosif, Viktor Kuncak, and Philipp Rümmer. 2012. A Verification Toolkit for Numerical Transition Systems - Tool Paper. In FM (LNCS, Vol. 7436). Springer, 247–251. https://doi.org/10.1007/978-3-642-32759-9_21 Google ScholarCross Ref
- Hossein Hojjat and Philipp Rümmer. 2018. The ELDARICA Horn Solver. In FMCAD. IEEE, 158–164. https://doi.org/10.23919/FMCAD.2018.8603013 Google ScholarCross Ref
- Bishoksan Kafle, John P. Gallagher, and Pierre Ganty. 2016. Solving non-linear Horn clauses using a linear Horn clause solver. In Proceedings 3rd Workshop on Horn Clauses for Verification and Synthesis, HCVS@ETAPS 2016, Eindhoven, The Netherlands, 3rd April 2016. 33–48. https://doi.org/10.4204/EPTCS.219.4 Google ScholarCross Ref
- Temesghen Kahsai, Rody Kersten, Philipp Rümmer, and Martin Schäf. 2017. Quantified Heap Invariants for Object-Oriented Programs. In LPAR (EPiC Series in Computing, Vol. 46). EasyChair, 368–384. https://easychair.org/publications/paper/PmhGoogle Scholar
- Temesghen Kahsai, Philipp Rümmer, Huascar Sanchez, and Martin Schäf. 2016. JayHorn: A Framework for Verifying Java programs. In CAV, Part I (LNCS, Vol. 9779). Springer, 352–358. https://doi.org/10.1007/978-3-319-41528-4_19 Google ScholarCross Ref
- Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno. 2011. Predicate abstraction and CEGAR for higher-order model checking. In ACM. ACM, 222–233. https://doi.org/10.1145/1993498.1993525 Google ScholarDigital Library
- Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. 2014. SMT-Based Model Checking for Recursive Programs. In CAV (LNCS, Vol. 8559). 17–34. https://doi.org/10.1007/978-3-319-08867-9_2 Google ScholarDigital Library
- Shuvendu K Lahiri, Akash Lal, Sridhar Gopinath, Alexander Nutz, Vladimir Levin, Rahul Kumar, Nate Deisinger, Jakob Lichtenberg, and Chetan Bansal. 2020. Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost. In FMCAD. IEEE. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_24 169–178. Google ScholarCross Ref
- Yusuke Matsushita, Takeshi Tsukada, and Naoki Kobayashi. 2020. RustHorn: CHC-Based Verification for Rust Programs. In ESOP, Peter Müller (Ed.) (LNCS, Vol. 12075). Springer, 484–514. https://doi.org/10.1007/978-3-030-44914-8_18 Google ScholarDigital Library
- Dmitry Mordvinov and Grigory Fedyukovich. 2017. Verifying Safety of Functional Programs with Rosette/Unbound. CoRR, abs/1704.04558 (2017), https://github.com/dvvrd/rosetteGoogle Scholar
- Saswat Padhi, Rahul Sharma, and Todd Millstein. 2016. Data-driven precondition inference with learned features. ACM SIGPLAN Notices, 51, 6 (2016), 42–56. https://doi.org/10.1145/2908080.2908099 Google ScholarDigital Library
- Sumanth Prabhu, Kumar Madhukar, and R Venkatesh. 2018. Efficiently learning safety proofs from appearance as well as behaviours. In SAS (LNCS, Vol. 11002). Springer, 326–343. https://doi.org/10.1007/978-3-319-99725-4_20 Google ScholarCross Ref
- Murali Krishna Ramanathan, Ananth Grama, and Suresh Jagannathan. 2007. Static specification inference using predicate mining. In PLDI. ACM, 123–134. https://doi.org/10.1145/1250734.1250749 Google ScholarDigital Library
- Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, and Cesare Tinelli. 2019. cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis. In CAV, Part II (LNCS, Vol. 11562). Springer, 74–83. https://doi.org/10.1007/978-3-030-25543-5_5 Google ScholarCross Ref
- Sriram Sankaranarayanan, Swarat Chaudhuri, Franjo Ivancic, and Aarti Gupta. 2008. Dynamic inference of likely data preconditions over predicates by tree learning. In Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2008, Seattle, WA, USA, July 20-24, 2008. 295–306. https://doi.org/10.1145/1390630.1390666 Google ScholarDigital Library
- Mohamed Nassim Seghir and Daniel Kroening. 2013. Counterexample-Guided Precondition Inference. In ESOP (Lecture Notes in Computer Science, Vol. 7792). Springer, 451–471. https://doi.org/10.1007/978-3-642-37036-6_25 Google ScholarDigital Library
- Sharon Shoham, Eran Yahav, Stephen Fink, and Marco Pistoia. 2007. Static specification mining using automata-based abstractions. In ISSTA. ACM, 174–184. https://doi.org/10.1145/1273463.1273487 Google ScholarDigital Library
- Jinlin Yang, David Evans, Deepali Bhardwaj, Thirumalesh Bhat, and Manuvir Das. 2006. Perracotta: mining temporal API rules from imperfect traces. In ICSE. ACM, 282–291. https://doi.org/10.1145/1134285.1134325 Google ScholarDigital Library
- Haiyan Zhu, Thomas Dillig, and Isil Dillig. 2013. Automated Inference of Library Specifications for Source-Sink Property Verification. In Programming Languages and Systems - 11th Asian Symposium, APLAS 2013, Melbourne, VIC, Australia, December 9-11, 2013. Proceedings. 290–306. https://doi.org/10.1007/978-3-319-03542-0_21 Google ScholarDigital Library
- He Zhu, Stephen Magill, and Suresh Jagannathan. 2018. A data-driven CHC solver. In PLDI. ACM, 707–721. https://doi.org/10.1145/3192366.3192416 Google ScholarDigital Library
Index Terms
- Specification synthesis with constrained Horn clauses
Recommendations
Synthesis of AMBA AHB from formal specification: a case study
The standard hardware design flow involves: (a) design of an integrated circuit using a hardware description language, (b) extensive functional and formal verification, and (c) logical synthesis. However, the above-mentioned processes consume ...
Formal specification and automated verification of UML2.0 sequence diagrams
GRC '12: Proceedings of the 2012 IEEE International Conference on Granular Computing (GrC-2012)Software reliability is with critical importance in security demanding areas, including space exploration, e-business and military defense. UML sequence diagrams capture the collaborations of objects, and bridge the gap between abstract design and ...
An Automatically Verified Prototype of the Tokeneer ID Station Specification
AbstractThe Tokeneer project was an initiative set forth by the National Security Agency (NSA, USA) to be used as a demonstration that developing highly secure systems can be made by applying rigorous methods in a cost-effective manner. Altran UK was ...
Comments