Powiadomienia systemowe
- Sesja wygasĹa!
- Sesja wygasĹa!
TytuĹ artykuĹu
Wybrane peĹne teksty z tego czasopisma
Identyfikatory
Warianty tytuĹu
JÄzyki publikacji
Abstrakty
In this article, we propose a symbolic technique that can be used for automatically inferring software contracts from programs that are written in a non-trivial fragment of C, called KERNEL C, that supports pointer-based structures and heap manipulation. Starting from the semantic definition of KERNEL C in the đ semantic framework, we enrich the symbolic execution facilities recently provided by đ with novel capabilities for contract synthesis that are based on abstract subsumption. Roughly speaking, we define an abstract symbolic technique that axiomatically explains the execution of any (modifier) C function by using other (observer) routines in the same program. We implemented our technique in the automated tool KIND SPEC 2.1, which generates logical axioms that express pre- and post-condition assertions which define the precise input/output behavior of the C routines. Thanks to the integrated support for symbolic execution and deductive verification provided by đ, some synthesized axioms that cannot be guaranteed to be correct by construction due to abstraction can finally be verified in our setting with little effort.
Wydawca
Czasopismo
Rocznik
Tom
Strony
235--273
Opis fizyczny
Bibliogr. 48 poz., rys., tab.
TwĂłrcy
autor
- VRAIN, Universitat Politècnica de València, Camino de Vera s/n, Valencia, Spain
autor
- DSIC, Universitat Politècnica de València, Valencia, Spain
autor
- VRAIN, Universitat Politècnica de València, Camino de Vera s/n, Valencia, Spain
Bibliografia
- [1] Meyer B. Applying âdesign by contractâ. Computer, 1992. 25(10):40-51. doi:10.1109/2.161279.
- [2] Cousot P, Cousot R, Fähndrich M, Logozzo F. Automatic Inference of Necessary Preconditions. In: 14th Intâl Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI 2013), volume 7737 of Lecture Notes in Computer Science. Springer, 2013 pp. 128-148. doi:10.1007/978-3-642-35873-9_10.
- [3] Ellison C, RoĹu G. An Executable Formal Semantics of C with Applications. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPLâ12). ACM, New York, 2012 pp. 533-544. doi:10.1145/2103656.2103719.
- [4] Cobleigh JM, Giannakopoulou D, PÄsÄreanu CS. Learning Assumptions for Compositional Verification. In: Proceedings of the 9th Intâl Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACASâ03), volume 2619 of Lecture Notes in Computer Science. Springer, Heidelberg, 2003 pp. 331-346. doi:10.1007/3-540-36577-X_24.
- [5] Alpuente M, FeliĂş MA, Villanueva A. Automatic Inference of Specifications Using Matching Logic. In: Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation (PEPMâ13). ACM, New York, 2013 pp. 127-136. doi:10.1145/2426890.2426914.
- [6] Alpuente M, Pardo D, Villanueva A. Automatic Inference of Specifications in the K Framework. Electronic Proc. in Theoretical Comp. Science, 2015. 200:1-17. doi:10.4204/EPTCS.200.1.
- [7] Liskov B, Guttag J. Abstraction and Specification in Program Development. MIT Press, Cambridge, MA, USA, 1986.
- [8] King JC. Symbolic Execution and Program Testing. Communications of the ACM, 1976. 19(7):385-394. doi:10.1145/360248.360252.
- [9] PÄsÄreanu CS, Visser W. A survey of new trends in symbolic execution for software testing and analysis. International Journal on Software Tools for Technology Transfer, 2009. 11(4):339-353. doi:10.1007/s10009-009-0118-1.
- [10] RoĹu G, ĹerbÄnuĹŁÄ TF. An overview of the K semantic framework. The Journal of Logic and Algebraic Programming, 2010. 79(6):397-434. doi:10.1016/j.jlap.2010.03.012.
- [11] RoĹu G, ĹtefÄnescu A. Matching Logic: A New Program Verification Approach (NIER Track). In: Proceedings of the 33rd Intâl Conf. on Software Engineering (ICSEâ11). ACM, New York, 2011 pp. 868-871. doi:10.1145/1985793.1985928.
- [12] ĹtefÄnescu A, Park D, Yuwen S, Li Y, RoĹu G. Semantics-based Program Verifiers for All Languages. In: Proceedings of the 2016 ACM SIGPLAN Intâl Conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLAâ16). ACM, 2016 pp. 74-91. doi:10.1145/2983990.2984027.
- [13] Arusoaie A, Lucanu D, Rusu V. Symbolic execution based on language transformation. Computer Languages, Systems & Structures, 2015. 44(A):48-71. doi:10.1016/j.cl.2015.08.004.
- [14] Anand S, PÄsÄreanu CS, Visser W. Symbolic execution with abstraction. International Journal on Software Tools for Technology Transfer, 2009. 11(1):53-67. doi:10.1007/s10009-008-0090-1.
- [15] Khurshid S, PÄsÄreanu CS, Visser W. Generalized Symbolic Execution for Model Checking and Testing. In: Proceedings of the 9th Intâl Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACASâ03). ACM, New York, 2003 pp. 553-568. doi:10.1007/3-540-36577-X_40.
- [16] Alpuente M, Pardo D, Villanueva A. Symbolic Abstract Contract Synthesis in a Rewriting Framework. In: Proceedings of the 26th Intâl Symposium on Logic-Based Program Synthesis and Transformation (LOPSTRâ16), volume 10184 of Lecture Notes in Computer Science. Springer, Cham, 2016 pp. 187-202. doi:10.1007/978-3-319-63139-4_11.
- [17] Moura Ld, Bjørner N. Z3: An Efficient SMT Solver. In: Proceedings of the 14th Intâl Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACASâ08), volume 4963 of Lecture Notes in Computer Science. Springer, Heidelberg, 2008 pp. 337-340. doi:10.1007/978-3-540-78800-3_24.
- [18] Baudin P, Cuoq P, Filliâtre JC, MarchÊ C, Monate B, Moy Y, Prevosto V. ACSL: ANSI/ISO C Specification Language, version 1.4, 2010.
- [19] Milner R. Communication and Concurrency. Prentice Hall, 1989.
- [20] Hähnle R, Baum M, Bubel R, Rothe M. A Visual Interactive Debugger Based on Symbolic Execution. In: Proceedings of the 25th IEEE/ACM Intâl Conf. on Automated Software Engineering (ASEâ10). ACM, New York, 2010 pp. 143-146. doi:10.1145/1858996.1859022.
- [21] Cousot P, Cousot R. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPLâ77). ACM, New York, 1977 pp. 238-252. doi:10.1145/512950.512973.
- [22] Manevich R, Yahav E, Ramalingam G, Sagiv S. Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists. In: Proceedings of the 6th Intâl Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAIâ05), volume 3385 of Lecture Notes in Computer Science. Springer, Heidelberg, 2005 pp. 181-198. doi:10.1007/978-3-540-30579-8_13.
- [23] Jaffar J, Navas JA, Santosa AE. Unbounded Symbolic Execution for Program Verification. In: Proceedings of the Second Intâl Conf. on Runtime Verification, RVâ11. Springer, Heidelberg. ISBN 978-3-642-29859-2, 2012 pp. 396-411. doi:10.1007/978-3-642-29860-8_32.
- [24] Padhi S, Sharma R, Millstein T. LoopInvGen: A Loop Invariant Generator based on Precondition Inference, 2017. URL https://arxiv.org/abs/1707.02029.
- [25] RoĹu G. From Rewriting Logic, to Programming Language Semantics, to Program Verification. In: Logic, Rewriting, and Concurrency: Essays dedicated to J. Meseguer on the occasion of his 65th Birthday, Lecture Notes in Comp. Sci., pp. 598-616. Springer, 2015. doi:10.1007/978-3-319-23165-5_28.
- [26] Reichel H. An approach to object semantics based on terminal co-algebras. Mathematical Structures in Computer Science, 1995. 5(2):129-152. doi:10.1017/S0960129500000694.
- [27] ĹtefÄnescu A, CiobâcÄ S, Moore B, ĹerbÄnuĹŁÄ TF, RoĹu G. Reachability Logic in K. Technical report, UIUC, 2013.
- [28] RoĹu G, ĹtefÄnescu A, CiobâcÄ S, Moore B. One-Path Reachability Logic. In: Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICSâ13). 2013 pp. 358-367. doi:10.1109/LICS.2013.42.
- [29] ĹtefÄnescu A, CiobâcÄ Ĺ, Mereuta R, Moore BM, ĹerbÄnutÄ TF, RoĹu G. All-Path Reachability Logic. In: Proceedings of the Joint 25th Intâl Conf. on Rewriting Techniques and Applications and 12th Intâl Conf. on Typed Lambda Calculi and Applications (RTA-TLCAâ14), volume 8560 of Lecture Notes in Computer Science. Springer, Cham, 2014 pp. 425-440. doi:10.1007/978-3-319-08918-8_29.
- [30] Magill S, Nanevski A, Clarke A, Lee P. Inferring invariants in Separation Logic for imperative list-processing programs. In: 3rd SPACE Workshop. 2006 doi:10.1.1.115.8677.
- [31] Calcagno C, Distefano D, OâHearn PW, Yang H. Footprint Analysis: A Shape Analysis That Discovers Preconditions. In: Proceedings of the 14th Intâl Static Analysis Symposium (SASâ07), volume 4634 of Lecture Notes in Computer Science. Springer, Heidelberg, 2007 pp. 402-418. doi:10.1007/978-3-540-74061-2_25.
- [32] Gulavani BS, Chakraborty S, Ramalingam G, Nori AV. Bottom-up Shape Analysis Using LISF. ACM Transactions on Programming Languages and Systems (TOPLAS), 2011. 33(5):17:1-17:41. doi:10.1145/2039346.2039349.
- [33] Moy Y, MarchĂŠ C. Modular inference of subprogram contracts for safety checking. Journal of Symbolic Computation, 2010. 45(11):1184-1211. doi:10.1016/j.jsc.2010.06.004.
- [34] Wei Y, Furia CA, Kazmin N, Meyer B. Inferring Better Contracts. In: Proceedings of the 33rd Intâl Conf. on Software Engineering (ICSEâ11). ACM, 2011 pp. 191-200. doi:10.1145/1985793.1985820.
- [35] Tillmann N, Chen F, Schulte W. Discovering Likely Method Specifications. In: Proceedings of the 8th Intâl Conf. on Formal Methods and Software Engineering (ICFEMâ06), volume 4260 of Lecture Notes in Computer Science. Springer, Heidelberg, 2006 pp. 717-736. doi:10.1007/11901433_39.
- [36] Ernst MD, Perkins JH, Guo PJ, McCamant S, Pacheco C, Tschantz MS, Xiao C. The Daikon system for dynamic detection of likely invariants. Science of Computer Programming, 2007. 69(1-3):35-45. doi:10.1016/j.scico.2007.01.015.
- [37] Hangal S, Lam MS. Tracking Down Software Bugs Using Automatic Anomaly Detection. In: Proceedings of the 24th Intâl Conf. on Software Engineering (ICSEâ02). ACM, New York, 2002 pp. 291-301. doi:10.1145/581339.581377.
- [38] Smallbone N, Johansson M, Claessen K, Algehed M. Quick specifications for the busy programmer. Journal on Functional Programming, 2017. 27:e18. doi:10.1017/S0956796817000090.
- [39] Henkel J, Reichenbach C, Diwan A. Discovering Documentation for Java Container Classes. IEEE Transactions on Software Engineering, 2007. 33(8):526-543. doi:10.1109/TSE.2007.70705.
- [40] Csallner C, Tillmann N, Smaragdakis Y. DySy: Dynamic Symbolic Execution for Invariant Inference. In: Proceedings of the 30th Intâl Conf. on Software Engineering (ICSEâ08). ACM, New York, 2008 pp.281-290. doi:10.1145/1368088.1368127.
- [41] Whaley J, Martin MC, Lam MS. Automatic Extraction of Object-oriented Component Interfaces. In: Proceedings of the 12th ACM SIGSOFT Intâl Symposium on Software Testing and Analysis (ISSTAâ02). ACM, New York, 2002 pp. 218-228. doi:10.1145/566171.566212.
- [42] Giannakopoulou D, PÄsÄreanu CS. Interface Generation and Compositional Verification in JavaPathfinder. In: Proceedings of the 12th Intâl Conf. on Fundamental Approaches to Software Engineering (FASEâ09), volume 5503 of Lecture Notes in Computer Science. Springer, Heidelberg, 2009 pp. 94-108. doi:10.1007/978-3-642-00593-0_7.
- [43] Bacci G, Comini M, FeliĂş MA, Villanueva A. Automatic Synthesis of Specifications for First Order Curry Programs. In: Proceedings of the 14th Symposium on Principles and Practice of Declarative Programming (PPDPâ12). ACM, New York, 2012 pp. 25-34. doi:10.1145/2370776.2370781.
- [44] Taghdiri M, Jackson D. Inferring specifications to detect errors in code. Automated Software Engineering, 2007. 14(1):87-121. doi:10.1007/s10515-006-0005-x.
- [45] Ghezzi C, Mocci A, Monga M. Synthesizing intensional behavior models by graph transformation. In: Proceedings of the IEEE 31st Intâl Conf. on Software Engineering (ICSEâ09). 2009 pp. 430-440. doi:10.1109/ICSE.2009.5070542.
- [46] Clavel M, DurĂĄn F, Eker S, Lincoln P, MartĂ-Oliet N, Meseguer J, Talcott CL (eds.). All About Maude â A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, volume 4350 of Lecture Notes in Computer Science. Springer, 2007.
- [47] Berdine J, Calcagno C, Cook B, Distefano D, OâHearn PW, Wies T, Yang H. Shape Analysis for Composite Data Structures. In: Proceedings of the 19th Intâl Conf. on Computer Aided Verification (CAVâ07), volume 4590 of Lecture Notes in Comp. Sci. Springer, Heidelberg, 2007 pp. 178-192. doi:10.1007/978-3-540-73368-3_22.
- [48] Distefano D, OâHearn PW, Yang H. A Local Shape Analysis Based on Separation Logic. In: Proceedings of the 12th Intâl Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACASâ06), volume 3920 of Lecture Notes in Comp. Sci. Springer, 2006 pp. 287-302. doi:10.1007/11691372_19.
Uwagi
Opracowanie rekordu ze ĹrodkĂłw MNiSW, umowa Nr 461252 w ramach programu "SpoĹeczna odpowiedzialnoĹÄ nauki" - moduĹ: Popularyzacja nauki i promocja sportu (2021).
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-f26b211d-c855-45f3-b03b-1d866d3b25a7