Syntax-driven program verification of matching logic properties
Authors: 
Domenico Bianculli, Antonio Filieri, 
Carlo Ghezzi, Dino Mandrioli, Alessandro Maria RizziAuthors Info & Claims
Pages 68 - 74
Abstract
We describe a novel approach to program verification and its application to verification of C programs, where properties are expressed in matching logic. The general approach is syntax-directed: semantic rules, expressed according to Knuth's attribute grammars, specify how verification conditions can be computed. Evaluation is performed by interplaying attribute computation and propagation through the syntax tree with invocation of a solver of logic formulae. The benefit of a general syntax-driven approach is that it provides a reusable reference scheme for implementing verifiers for different languages. We show that the instantiation of a general approach to a specific language does not penalize the efficiency of the resulting verifier. This is done by comparing our C verifier for matching logic with an existing tool for the same programming language and logic. A further key advantage of the syntax-directed approach is that it can be the starting point for an incremental verifier---which is our long-term research target.
References
[1]
J. C. Reynolds, "Separation logic: A logic for shared mutable data structures," in Proc. of LICS '02. IEEE, 2002, pp. 55--74.
[2]
G. Roşu, C. Ellison, and W. Schulte, "Matching logic: An alternative to Hoare/Floyd logic," in Proc. of AMAST '10, ser. LNCS, vol. 6486, 2010, pp. 142--162.
[3]
D. Beyer, T. Henzinger, R. Jhala, and R. Majumdar, "The software model checker blast," STTT, vol. 9, pp. 505--525, 2007.
[4]
W. Visser, K. Havelund, G. Brat, S. Park, and F. Lerda, "Model checking programs," JASE, vol. 10, no. 2, pp. 203--232, 2003.
[5]
C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata, "Extended static checking for Java," in Proc. of PLDI '02. ACM, 2002, pp. 234--245.
[6]
M. Barnett, B.-Y. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino, "Boogie: A modular reusable verifier for object-oriented programs," in Proc. of FMCO '05, ser. LCNS. Springer, 2006, vol. 4111, pp. 364--387.
[7]
L. De Moura and N. Bjørner, "Z3: An efficient SMT solver," in Proc. of TACAS'08/ETAPS'08. Springer, 2008, pp. 337--340.
[8]
D. Knuth, "Semantics of context-free languages," Mathematical systems theory, vol. 2, no. 2, pp. 127--145, 1968.
[9]
A. Barenghi, S. Crespi Reghizzi, D. Mandrioli, and M. Pradella, "Parallel parsing of operator precedence grammars," Inf. Process. Lett., vol. 113, no. 7, pp. 245--249, 2013.
[10]
D. Bianculli, A. Filieri, C. Ghezzi, and D. Mandrioli, "Syntactic-semantic incrementality for agile verification," Sci. Comput. Program., vol. 97, part 1, no. 0, pp. 47--54, 2015.
[11]
D. Bianculli, A. Filieri, C. Ghezzi, and D. Mandrioli, "Incremental syntactic-semantic reliability analysis of evolving structured workflows," in Proc. of ISOLA 2014, ser. LNCS. Springer, 2014, vol. 8802, pp. 41--55.
[12]
A. Ştefănescu, "MatchC: A matching logic reachability verifier using the framework," Electron. Notes Theor. Comput. Sci., vol. 304, no. 0, pp. 183--198, 2014.
[13]
G. Roşu and A. Ştefănescu, "Checking reachability using matching logic," in Proc. of OOPSLA'12. ACM, 2012, pp. 555--574.
[14]
C. Ghezzi, "Evolution, adaptation, and the quest for incrementality," in Proc. of the 17th Monterey Workshop, ser. LNCS, vol. 7539. Springer, 2012, pp. 369--379.
[15]
C. Ghezzi and D. Mandrioli, "Incremental parsing," ACM Trans. Program. Lang. Syst., vol. 1, no. 1, pp. 58--70, 1979.
[16]
G. Roşu and T. F. Şerbănuţă, "An overview of the K semantic framework," J. LAP, vol. 79, no. 6, pp. 397--434, 2010.
[17]
A. M. Rizzi, "Incremental reachability checking of KernelC programs using matching logic," in Companion of ICSE'14 Proc. ACM, 2014, pp. 724--726.
Index Terms
- Syntax-driven program verification of matching logic properties
Recommendations
Syntax-Driven Program Verification of Matching Logic Properties
FORMALISE '15: Proceedings of the 2015 IEEE/ACM 3rd FME Workshop on Formal Methods in Software EngineeringWe describe a novel approach to program verification and its application to verification of C programs, where properties are expressed in matching logic. The general approach is syntax-directed: semantic rules, expressed according to Knuth's attribute ...
Completeness and expressiveness of pointer program verification by separation logic
AbstractReynolds' separation logical system for pointer program verification is investigated. This paper proves its completeness theorem that states that every true asserted program is provable in the logical system. In order to prove the ...
Coinductive Verification of Program Optimizations Using Similarity Relations
Formal verification methods have gained increased importance due to their ability to guarantee system correctness and improve reliability. Nevertheless, the question how proofs are to be formalized in theorem provers is far from being trivial, yet very ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Sponsors
- ACM: Association for Computing Machinery
- SIGSOFT: ACM Special Interest Group on Software Engineering
- IEEE-CS\DATC: IEEE Computer Society
- TCSE: IEEE Computer Society's Tech. Council on Software Engin.
Publisher
IEEE Press
Publication History
Published: 16 May 2015
Check for updates
Qualifiers
- Research-article
Conference
Upcoming Conference
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 57Total Downloads
- Downloads (Last 12 months)2
- Downloads (Last 6 weeks)0
Reflects downloads up to 23 Sep 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in