Search Results

Documents authored by Reilles, Antoine


Document
Formal Validation of Pattern Matching code

Authors: Claude Kirchner, Pierre-Etienne Moreau, and Antoine Reilles

Published in: OASIcs, Volume 3, Workshop on Trustworthy Software (2006)


Abstract
When addressing the formal validation of generated software, two main alternatives consist either to prove the correctness of compilers or to directly validate the generated code. Here, we focus on directly proving the correctness of compiled code issued from powerful pattern matching constructions typical of ML like languages or rewrite based languages such as ELAN, MAUDE or Tom. In this context, our first contribution is to define a general framework for anchoring algebraic pattern-matching capabilities in existing languages like C, Java or ML. Then, using a just enough powerful intermediate language, we formalize the behavior of compiled code and define the correctness of compiled code with respect to pattern-matching behavior. This allows us to prove the equivalence of compiled code correctness with a generic first-order proposition whose proof could be achieved via a proof assistant or an automated theorem prover. We then extend these results to the multi-match situation characteristic of the ML like languages. The whole approach has been implemented on top of the Tom compiler and used to validate the syntactic matching code of the Tom compiler itself.

Cite as

Claude Kirchner, Pierre-Etienne Moreau, and Antoine Reilles. Formal Validation of Pattern Matching code. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)


Copy BibTex To Clipboard

@InProceedings{kirchner_et_al:OASIcs.TrustworthySW.2006.697,
  author =	{Kirchner, Claude and Moreau, Pierre-Etienne and Reilles, Antoine},
  title =	{{Formal Validation of Pattern Matching code}},
  booktitle =	{Workshop on Trustworthy Software},
  pages =	{1--22},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-02-6},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{3},
  editor =	{Autexier, Serge and Merz, Stephan and van der Torre, Leon and Wilhelm, Reinhard and Wolper, Pierre},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TrustworthySW.2006.697},
  URN =		{urn:nbn:de:0030-drops-6978},
  doi =		{10.4230/OASIcs.TrustworthySW.2006.697},
  annote =	{Keywords: Correctness proofs, compilers, pattern matching, validation}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail