Rewriting modulo SMT and open system analysis

This paper proposes rewriting modulo SMT, a new technique that combines the power of SMT solving, rewriting modulo theories, and model checking. Rewriting modulo SMT is ideally suited to model and analyze reachability properties of infinite-state open systems, i.e., systems that interact with a nond...

Full description

Autores:
Rocha, Camilo
Meseguer, José
Muñoz, César
Tipo de recurso:
Article of journal
Fecha de publicación:
2016
Institución:
Escuela Colombiana de Ingeniería Julio Garavito
Repositorio:
Repositorio Institucional ECI
Idioma:
eng
OAI Identifier:
oai:repositorio.escuelaing.edu.co:001/1866
Acceso en línea:
https://repositorio.escuelaing.edu.co/handle/001/1866
Palabra clave:
Relaciones de conjuntos sincrónicos
Semántica síncrona
Reescritura de lógica
Simulación formal y verificación
Synchronous set relations
Synchronous semantics
Rewriting logic
Formal simulation and verification
PLEXIL
Rights
openAccess
License
© 2016 Elsevier Inc. All rights reserved.
id ESCUELAIG2_bfc2cf9dcade11e9fc538723d92c7370
oai_identifier_str oai:repositorio.escuelaing.edu.co:001/1866
network_acronym_str ESCUELAIG2
network_name_str Repositorio Institucional ECI
repository_id_str
dc.title.eng.fl_str_mv Rewriting modulo SMT and open system analysis
title Rewriting modulo SMT and open system analysis
spellingShingle Rewriting modulo SMT and open system analysis
Relaciones de conjuntos sincrónicos
Semántica síncrona
Reescritura de lógica
Simulación formal y verificación
Synchronous set relations
Synchronous semantics
Rewriting logic
Formal simulation and verification
PLEXIL
title_short Rewriting modulo SMT and open system analysis
title_full Rewriting modulo SMT and open system analysis
title_fullStr Rewriting modulo SMT and open system analysis
title_full_unstemmed Rewriting modulo SMT and open system analysis
title_sort Rewriting modulo SMT and open system analysis
dc.creator.fl_str_mv Rocha, Camilo
Meseguer, José
Muñoz, César
dc.contributor.author.none.fl_str_mv Rocha, Camilo
Meseguer, José
Muñoz, César
dc.contributor.researchgroup.spa.fl_str_mv Informática
dc.subject.armarc.spa.fl_str_mv Relaciones de conjuntos sincrónicos
Semántica síncrona
Reescritura de lógica
Simulación formal y verificación
topic Relaciones de conjuntos sincrónicos
Semántica síncrona
Reescritura de lógica
Simulación formal y verificación
Synchronous set relations
Synchronous semantics
Rewriting logic
Formal simulation and verification
PLEXIL
dc.subject.proposal.eng.fl_str_mv Synchronous set relations
Synchronous semantics
Rewriting logic
Formal simulation and verification
PLEXIL
description This paper proposes rewriting modulo SMT, a new technique that combines the power of SMT solving, rewriting modulo theories, and model checking. Rewriting modulo SMT is ideally suited to model and analyze reachability properties of infinite-state open systems, i.e., systems that interact with a nondeterministic environment. Such systems exhibit both internal nondeterminism, which is proper to the system, and external nondeterminism, which is due to the environment. In a reflective formalism, such as rewriting logic, rewriting modulo SMT can be reduced to standard rewriting. Hence, rewriting modulo SMT naturally extends rewriting-based reachability analysis techniques, which are available for closed systems, to open systems. Furthermore, a single state expression with symbolic constraints can now denote an infinite set of concrete states. The proposed technique is illustrated with the formal analysis of: (i) a real-time system that is beyond the scope of timed-automata methods and (ii) automatic detection of reachability violations in a synchronous language developed to support autonomous spacecraft operations.
publishDate 2016
dc.date.issued.none.fl_str_mv 2016
dc.date.accessioned.none.fl_str_mv 2021-11-27T17:07:35Z
dc.date.available.none.fl_str_mv 2021-11-27T17:07:35Z
dc.type.spa.fl_str_mv Artículo de revista
dc.type.coar.fl_str_mv http://purl.org/coar/resource_type/c_2df8fbb1
dc.type.coarversion.fl_str_mv http://purl.org/coar/version/c_970fb48d4fbd8a85
dc.type.version.spa.fl_str_mv info:eu-repo/semantics/publishedVersion
dc.type.coar.spa.fl_str_mv http://purl.org/coar/resource_type/c_6501
dc.type.content.spa.fl_str_mv Text
dc.type.driver.spa.fl_str_mv info:eu-repo/semantics/article
dc.type.redcol.spa.fl_str_mv http://purl.org/redcol/resource_type/ART
format http://purl.org/coar/resource_type/c_6501
status_str publishedVersion
dc.identifier.issn.none.fl_str_mv 01676423
dc.identifier.uri.none.fl_str_mv https://repositorio.escuelaing.edu.co/handle/001/1866
identifier_str_mv 01676423
url https://repositorio.escuelaing.edu.co/handle/001/1866
dc.language.iso.spa.fl_str_mv eng
language eng
dc.relation.citationendpage.spa.fl_str_mv 297
dc.relation.citationissue.spa.fl_str_mv 1
dc.relation.citationstartpage.spa.fl_str_mv 269
dc.relation.citationvolume.spa.fl_str_mv 86
dc.relation.indexed.spa.fl_str_mv N/A
dc.relation.ispartofjournal.eng.fl_str_mv Journal of Logical and Algebraic Methods in Programming
dc.relation.references.spa.fl_str_mv E. Althaus, E. Kruglov, C. Weidenbach, Superposition modulo linear arithmetic SUP(LA), in: 7th International Symposium on Frontiers of Combining Systems, in: Lect. Notes Comput. Sci., vol. 5749, Springer, 2009, pp. 84–99.
R. Alur, D.L. Dill, A theory of timed automata, Theor. Comput. Sci. 126 (2) (1994) 183–235.
A. Armando, J. Mantovani, L. Platania, Bounded model checking of software using SMT solvers instead of SAT solvers, Int. J. Softw. Tools Technol. Transf. 11 (1) (2009) 69–83.
A. Arusoaie, D. Lucanu, V. Rusu, A generic framework for symbolic execution, in: 6th International Conference on Software Language Engineering, in: Lect. Notes Comput. Sci., vol. 8225, Springer, 2013, pp. 281–301.
M. Ayala-Rincón, Expressiveness of Conditional Equational Systems with Built-in Predicates, PhD thesis, Universität Kaiserslauten, 1993.
F. Baader, T. Nipkow, Term Rewriting and All That, Cambridge University Press, 1998.
F. Baader, K. Schulz, Unification in the union of disjoint equational theories: combining decision procedures, J. Symb. Comput. 21 (1996) 211–243.
K. Bae, S. Escobar, J. Meseguer, Abstract logical model checking of infinite-state systems using narrowing, in: 24th International Conference on Rewriting Techniques and Applications, in: Leibniz International Proceedings in Informatics, vol. 21, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2013, pp. 81–96.
K. Bae, C. Rocha, A note on symbolic reachability analysis modulo integer constraints for the CASH algorithm, available at http://maude.cs.uiuc.edu/ cases/scash, 2012.
M.P. Bonacina, C. Lynch, L.M. de Moura, On deciding satisfiability by theorem proving with speculative inferences, J. Autom. Reason. 47 (2) (2011) 161–189.
A. Boudet, Combining unification algorithms, J. Symb. Comput. 16 (6) (1993) 597–626.
A. Bouhoula, F. Jacquemard, Automated induction with constrained tree automata, in: 4th International Joint Conference on Automated Reasoning, in: Lect. Notes Comput. Sci., vol. 5195, Springer, 2008, pp. 539–554.
A. Bouhoula, F. Jacquemard, Sufficient completeness verification for conditional and constrained TRS, J. Appl. Log. 10 (1) (2012) 127–143, Special issue on Automated Specification and Verification of Web Systems.
R. Bruni, J. Meseguer, Semantic foundations for generalized rewrite theories, Theor. Comput. Sci. 360 (1–3) (2006) 386–414.
M. Caccamo, G.C. Buttazzo, L. Sha, Capacity sharing for overrun control, in: IEEE 34th Real-Time Systems Symposium, IEEE Computer Society, 2000, pp. 295–304.
C. Cadar, D. Dunbar, D.R. Engler, KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs, in: 8th USENIX Symposium on Operating Systems Design and Implementation, USENIX Association, 2008, pp. 209–224.
C. Cadar, K. Sen, Symbolic execution for software testing: three decades later, Commun. ACM 56 (2) (Feb. 2013) 82–90.
A. Cimatti, A. Griggio, Software model checking via IC3, in: 24th International Conference on Computer Aided Verification, in: Lect. Notes Comput. Sci., vol. 7358, Springer, 2012, pp. 277–293.
M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, C.L. Talcott, All About Maude – A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, Lect. Notes Comput. Sci., vol. 4350, Springer, 2007.
M. Clavel, J. Meseguer, M. Palomino, Reflection in membership equational logic, many-sorted equational logic, horn logic with equality, and rewriting logic, Theor. Comput. Sci. 373 (1–2) (2007) 70–91.
G. Delzanno, A. Podelski, Constraint-based deductive model checking, Int. J. Softw. Tools Technol. Transf. 3 (3) (2001) 250–270.
G. Dowek, C. Muñoz, C. Pas˘ areanu, ˘ A formal analysis framework for PLEXIL, in: 3rd Workshop on Planning and Plan Execution for Real-World Systems, September 2007, pp. 45–51.
[23] G. Dowek, C. Muñoz, C. Pas˘ areanu, ˘ A Small-Step Semantics of PLEXIL, Technical Report 2008-11, National Institute of Aerospace, Hampton, VA, 2008.
G. Dowek, C.A. Muñoz, C. Rocha, Rewriting logic semantics of a plan execution language, in: 6th Workshop on Structural Operational Semantics, in: Electron. Proc. Theor. Comput. Sci., vol. 18, 2009, pp. 77–91.
F. Durán, S. Lucas, C. Marché, J. Meseguer, X. Urbain, Proving operational termination of membership equational programs, High.-Order Symb. Comput. 21 (1–2) (2008) 59–88.
T. Estlin, A. Jónsson, C. Pas˘ areanu, ˘ R. Simmons, K. Tso, V. Verma, Plan Execution Interchange Language (PLEXIL), Technical Memorandum TM-2006-213483, NASA, 2006.
S. Falke, D. Kapur, Dependency pairs for rewriting with built-in numbers and semantic data structures, in: 19th International Conference on Rewriting Techniques and Applications, in: Lect. Notes Comput. Sci., vol. 5117, Springer, Berlin, Heidelberg, 2008, pp. 94–109.
S. Falke, D. Kapur, Operational termination of conditional rewriting with built-in numbers and semantic data structures, Electron. Notes Theor. Comput. Sci. 237 (2009) 75–90.
S. Falke, D. Kapur, Rewriting induction + linear arithmetic = decision procedure, in: 6th International Joint Conference on Automated Reasoning, in: Lect. Notes Comput. Sci., vol. 7364, Springer, 2012, pp. 241–255.
M. Ganai, A. Gupta, Accelerating high-level bounded model checking, in: 2006 IEEE/ACM International Conference on Computer Aided Design, Nov. 2006, pp. 794–801.
H. Ganzinger, R. Nieuwenhuis, Constraints and theorem proving, in: Constraints in Computational Logics: Theory and Applications, International Sum mer School, in: Lect. Notes Comput. Sci., vol. 2002, Springer, 1999, pp. 159–201.
T. Genet, T. Le Gall, A. Legay, V. Murat, A completion algorithm for lattice tree automata, in: 18th International Conference on Implementation and Application of Automata, in: Lect. Notes Comput. Sci., vol. 7982, Springer, 2013, pp. 134–145.
S. Ghilardi, E. Nicolini, S. Ranise, D. Zucchelli, Combination methods for satisfiability and model-checking of infinite-state systems, in: 21st International Conference on Automated Deduction, in: Lect. Notes Comput. Sci., vol. 4603, Springer, 2007, pp. 362–378.
S. Ghilardi, E. Nicolini, S. Ranise, D. Zucchelli, Towards SMT model checking of array-based systems, in: 4th International Joint Conference on Automated Reasoning, in: Lect. Notes Comput. Sci., vol. 5195, Springer, 2008, pp. 67–82.
S. Ghilardi, S. Ranise, MCMT: a model checker modulo theories, in: 5th International Joint Conference on Automated Reasoning, in: Lect. Notes Comput. Sci., vol. 6173, Springer, 2010, pp. 22–29.
J.A. Goguen, J. Meseguer, Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations, Theor. Comput. Sci. 105 (2) (1992) 217–273.
H. Hojjat, P. Rümmer, P. Subotic, W. Yi, Horn clauses for communicating timed systems, in: N. Bjørner, F. Fioravanti, A. Rybalchenko, V. Senni (Eds.), 1st Workshop on Horn Clauses for Verification and Synthesis, in: Electron. Proc. Theor. Comput. Sci., vol. 169, 2014, pp. 39–52.
H. Kirchner, C. Ringeissen, Combining symbolic constraint solvers on algebraic domains, J. Symb. Comput. 18 (2) (1994) 113–155.
K. Kirchner, H. Kirchner, M. Rusinowitch, Deduction with symbolic constraints, Rev. Intell. Artif. 4 (3) (1990) 9–52.
C. Kop, N. Nishida, Term rewriting with logical constraints, in: 9th International Symposium on Frontiers of Combining Systems, in: Lect. Notes Comput. Sci., vol. 8152, Springer, 2013, pp. 343–358.
C. Kop, N. Nishida, Automatic constrained rewriting induction towards verifying procedural programs, in: 12th Asian Symposium on Programming Languages and Systems, in: Lect. Notes Comput. Sci., vol. 8858, Springer, 2014, pp. 334–353.
[42] A. Lal, S. Qadeer, S. Lahiri, Corral: A Solver for Reachability Modulo Theories, Technical Report MSR-TR-2012-9, Microsoft Research, January 2012.
K.G. Larsen, P. Pettersson, W. Yi, UPPAAL in a nutshell, Int. J. Softw. Tools Technol. Transf. 1 (1–2) (1997) 134–152.
D. Lucanu, T.-F. Serbanuta, G. Rosu, K framework distilled, in: 9th International Workshop on Rewriting Logic and Its Applications, in: Lect. Notes Comput. Sci., vol. 7571, Springer, 2012, pp. 31–53.
S. Lucas, J. Meseguer, Operational termination of membership equational programs: the order-sorted way, Electron. Notes Theor. Comput. Sci. 238 (3) (2009) 207–225.
J. Meseguer, Conditional rewriting logic as a unified model of concurrency, Theor. Comput. Sci. 96 (1) (1992) 73–155.
J. Meseguer, Membership algebra as a logical framework for equational specification, in: 12th International Workshop on Recent Trends in Algebraic Development Techniques, in: Lect. Notes Comput. Sci., vol. 1376, Springer, 1997, pp. 18–61.
J. Meseguer, P. Thati, Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols, High.-Order Symb. Comput. 20 (1–2) (2007) 123–160.
A. Milicevic, H. Kugler, Model checking using SMT and theory of lists, in: NASA 3rd International Symposium on Formal Methods, in: Lect. Notes Comput. Sci., vol. 6617, Springer, 2011, pp. 282–297.
G. Nelson, D.C. Oppen, Simplification by cooperating decision procedures, ACM Trans. Program. Lang. Syst. 1 (2) (1979) 245–257.
R. Nieuwenhuis, A. Oliveras, C. Tinelli, Solving SAT and SAT modulo theories: from an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T ), J. ACM 53 (6) (2006) 937–977.
P.C. Ölveczky, M. Caccamo, Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude, in: L. Baresi, R. Heckel (Eds.), 9th International Conference on Fundamental Approaches to Software Engineering, in: Lect. Notes Comput. Sci., vol. 3922, Springer, 2006, pp. 357–372.
S. Owre, J. Rushby, N. Shankar, PVS: a prototype verification system, in: 11th International Conference on Automated Deduction, in: Lect. Notes Artif. Intell., vol. 607, Springer-Verlag, Saratoga, NY, June 1992, pp. 748–752.
A. Podelski, Model checking as constraint solving, in: 7th International Symposium on Static Analysis, in: Lect. Notes Comput. Sci., vol. 1824, Springer, 2000, pp. 22–37.
C. Rocha, Symbolic Reachability Analysis for Rewrite Theories, PhD thesis, University of Illinois at Urbana-Champaign, 2012.
C. Rocha, H. Cadavid, C.A. Muñoz, R. Siminiceanu, A formal interactive verification environment for the Plan Execution Interchange Language, in: 9th International Conference on Integrated Formal Methods, in: Lect. Notes Comput. Sci., vol. 7321, Springer, 2012, pp. 343–357.
C. Rocha, J. Meseguer, C. Muñoz, Rewriting Modulo SMT, Technical Memorandum NASA/TM-2013-218033, NASA Langley Research Center, Hampton, VA, August 2013.
C. Rocha, J. Meseguer, C. Muñoz, Rewriting modulo SMT and open system analysis, in: 10th International Workshop on Rewriting Logic and Its Appli cations, in: Lect. Notes Comput. Sci., vol. 8663, Springer International Publishing, 2014, pp. 247–262
G. Ro ¸su, A. Stef ¸ anescu, ˘ Matching logic: a new program verification approach, in: 33rd International Conference on Software Engineering, ACM, New York, NY, USA, 2011, pp. 868–871.
T. Rybina, A. Voronkov, A logical reconstruction of reachability, in: 5th International Andrei Ershov Memorial Conference on Perspectives of Systems Informatics, in: Lect. Notes Comput. Sci., vol. 2890, Springer, 2003, pp. 222–237.
T. Sakata, N. Nishida, T. Sakabe, On proving termination of constrained term rewrite systems by eliminating edges from dependency graphs, in: 20th International Workshop on Functional and Constraint Logic Programming, in: Lect. Notes Comput. Sci., vol. 6816, Springer, 2011, pp. 138–155.
P. Thati, J. Meseguer, Complete symbolic reachability analysis using back-and-forth narrowing, Theor. Comput. Sci. 366 (1–2) (2006) 163–179.
M. Veanes, N. Bjørner, A. Raschke, An SMT approach to bounded reachability analysis of model programs, in: 28th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems, Springer, 2008, pp. 53–68.
G. Vidal, Closed symbolic execution for verifying program termination, in: IEEE 12th International Working Conference on Source Code Analysis and Manipulation, Sept 2012, pp. 34–43.
G. Vidal, Symbolic execution as a basis for termination analysis, Sci. Comput. Program. 102 (2015) 142–157
P. Viry, Equational rules for rewriting logic, Theor. Comput. Sci. 285 (2002) 487–517.
D. Walter, S. Little, C. Myers, Bounded model checking of analog and mixed-signal circuits using an SMT solver, in: 5th International Symposium on Automated Technology for Verification and Analysis, Springer, Berlin, Heidelberg, 2007, pp. 66–81.
S. Yovine, KRONOS: a verification tool for real-time systems, Int. J. Softw. Tools Technol. Transf. 1 (1) (1997) 123–133
dc.rights.eng.fl_str_mv © 2016 Elsevier Inc. All rights reserved.
dc.rights.coar.fl_str_mv http://purl.org/coar/access_right/c_abf2
dc.rights.uri.spa.fl_str_mv https://creativecommons.org/licenses/by/4.0/
dc.rights.accessrights.spa.fl_str_mv info:eu-repo/semantics/openAccess
dc.rights.creativecommons.spa.fl_str_mv Atribución 4.0 Internacional (CC BY 4.0)
rights_invalid_str_mv © 2016 Elsevier Inc. All rights reserved.
https://creativecommons.org/licenses/by/4.0/
Atribución 4.0 Internacional (CC BY 4.0)
http://purl.org/coar/access_right/c_abf2
eu_rights_str_mv openAccess
dc.format.extent.spa.fl_str_mv 29 páginas.
dc.format.mimetype.spa.fl_str_mv application/pdf
dc.publisher.spa.fl_str_mv Elsevier
dc.source.spa.fl_str_mv https://www.sciencedirect.com/science/article/pii/S2352220816301195
institution Escuela Colombiana de Ingeniería Julio Garavito
bitstream.url.fl_str_mv https://repositorio.escuelaing.edu.co/bitstream/001/1866/1/Rewriting%20modulo%20SMT%20and%20open%20system%20analysis.pdf
https://repositorio.escuelaing.edu.co/bitstream/001/1866/2/license.txt
https://repositorio.escuelaing.edu.co/bitstream/001/1866/3/Rewriting%20modulo%20SMT%20and%20open%20system%20analysis.pdf.txt
https://repositorio.escuelaing.edu.co/bitstream/001/1866/4/Rewriting%20modulo%20SMT%20and%20open%20system%20analysis.pdf.jpg
bitstream.checksum.fl_str_mv cc4ae003726dfd863f39bb4e5d6935f5
5a7ca94c2e5326ee169f979d71d0f06e
d1d03a6aa8d96400131fa8abe6cb763f
60b583e806acbcefb9b4cde7a889fb31
bitstream.checksumAlgorithm.fl_str_mv MD5
MD5
MD5
MD5
repository.name.fl_str_mv Repositorio Escuela Colombiana de Ingeniería Julio Garavito
repository.mail.fl_str_mv repositorio.eci@escuelaing.edu.co
_version_ 1814355582693408768
spelling Rocha, Camilo649eba80a4c919beefa7d19955bc2950600Meseguer, José6da02984a567cfba226ed9b8bf7c47c0600Muñoz, César70953c4ce36fbd95e2df915d4688e3b1600Informática2021-11-27T17:07:35Z2021-11-27T17:07:35Z201601676423https://repositorio.escuelaing.edu.co/handle/001/1866This paper proposes rewriting modulo SMT, a new technique that combines the power of SMT solving, rewriting modulo theories, and model checking. Rewriting modulo SMT is ideally suited to model and analyze reachability properties of infinite-state open systems, i.e., systems that interact with a nondeterministic environment. Such systems exhibit both internal nondeterminism, which is proper to the system, and external nondeterminism, which is due to the environment. In a reflective formalism, such as rewriting logic, rewriting modulo SMT can be reduced to standard rewriting. Hence, rewriting modulo SMT naturally extends rewriting-based reachability analysis techniques, which are available for closed systems, to open systems. Furthermore, a single state expression with symbolic constraints can now denote an infinite set of concrete states. The proposed technique is illustrated with the formal analysis of: (i) a real-time system that is beyond the scope of timed-automata methods and (ii) automatic detection of reachability violations in a synchronous language developed to support autonomous spacecraft operations.Este artículo propone la reescritura de módulo SMT, una nueva técnica que combina el poder de la resolución SMT, la reescritura de teorías de módulo y la verificación de modelos. La reescritura del módulo SMT es ideal para modelar y analizar las propiedades de accesibilidad de los sistemas abiertos de estado infinito, es decir, los sistemas que interactúan con un entorno no determinista. Dichos sistemas exhiben tanto un no determinismo interno, que es propio del sistema, como un no determinismo externo, que se debe al entorno. En un formalismo reflexivo, como la lógica de reescritura, la reescritura del módulo SMT se puede reducir a la reescritura estándar. Por lo tanto, la reescritura del módulo SMT extiende naturalmente las técnicas de análisis de accesibilidad basadas en la reescritura, que están disponibles para sistemas cerrados, a sistemas abiertos. Además, una sola expresión de estado con restricciones simbólicas ahora puede denotar un conjunto infinito de estados concretos. La técnica propuesta se ilustra con el análisis formal de: (i) un sistema en tiempo real que está más allá del alcance de los métodos de autómatas cronometrados y (ii) detección automática de violaciones de accesibilidad en un lenguaje sincrónico desarrollado para soportar operaciones de naves espaciales autónomas.29 páginas.application/pdfengElsevier© 2016 Elsevier Inc. All rights reserved.https://creativecommons.org/licenses/by/4.0/info:eu-repo/semantics/openAccessAtribución 4.0 Internacional (CC BY 4.0)http://purl.org/coar/access_right/c_abf2https://www.sciencedirect.com/science/article/pii/S2352220816301195Rewriting modulo SMT and open system analysisArtículo de revistainfo:eu-repo/semantics/publishedVersionhttp://purl.org/coar/resource_type/c_6501http://purl.org/coar/resource_type/c_2df8fbb1Textinfo:eu-repo/semantics/articlehttp://purl.org/redcol/resource_type/ARThttp://purl.org/coar/version/c_970fb48d4fbd8a85297126986N/AJournal of Logical and Algebraic Methods in ProgrammingE. Althaus, E. Kruglov, C. Weidenbach, Superposition modulo linear arithmetic SUP(LA), in: 7th International Symposium on Frontiers of Combining Systems, in: Lect. Notes Comput. Sci., vol. 5749, Springer, 2009, pp. 84–99.R. Alur, D.L. Dill, A theory of timed automata, Theor. Comput. Sci. 126 (2) (1994) 183–235.A. Armando, J. Mantovani, L. Platania, Bounded model checking of software using SMT solvers instead of SAT solvers, Int. J. Softw. Tools Technol. Transf. 11 (1) (2009) 69–83.A. Arusoaie, D. Lucanu, V. Rusu, A generic framework for symbolic execution, in: 6th International Conference on Software Language Engineering, in: Lect. Notes Comput. Sci., vol. 8225, Springer, 2013, pp. 281–301.M. Ayala-Rincón, Expressiveness of Conditional Equational Systems with Built-in Predicates, PhD thesis, Universität Kaiserslauten, 1993.F. Baader, T. Nipkow, Term Rewriting and All That, Cambridge University Press, 1998.F. Baader, K. Schulz, Unification in the union of disjoint equational theories: combining decision procedures, J. Symb. Comput. 21 (1996) 211–243.K. Bae, S. Escobar, J. Meseguer, Abstract logical model checking of infinite-state systems using narrowing, in: 24th International Conference on Rewriting Techniques and Applications, in: Leibniz International Proceedings in Informatics, vol. 21, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2013, pp. 81–96.K. Bae, C. Rocha, A note on symbolic reachability analysis modulo integer constraints for the CASH algorithm, available at http://maude.cs.uiuc.edu/ cases/scash, 2012.M.P. Bonacina, C. Lynch, L.M. de Moura, On deciding satisfiability by theorem proving with speculative inferences, J. Autom. Reason. 47 (2) (2011) 161–189.A. Boudet, Combining unification algorithms, J. Symb. Comput. 16 (6) (1993) 597–626.A. Bouhoula, F. Jacquemard, Automated induction with constrained tree automata, in: 4th International Joint Conference on Automated Reasoning, in: Lect. Notes Comput. Sci., vol. 5195, Springer, 2008, pp. 539–554.A. Bouhoula, F. Jacquemard, Sufficient completeness verification for conditional and constrained TRS, J. Appl. Log. 10 (1) (2012) 127–143, Special issue on Automated Specification and Verification of Web Systems.R. Bruni, J. Meseguer, Semantic foundations for generalized rewrite theories, Theor. Comput. Sci. 360 (1–3) (2006) 386–414.M. Caccamo, G.C. Buttazzo, L. Sha, Capacity sharing for overrun control, in: IEEE 34th Real-Time Systems Symposium, IEEE Computer Society, 2000, pp. 295–304.C. Cadar, D. Dunbar, D.R. Engler, KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs, in: 8th USENIX Symposium on Operating Systems Design and Implementation, USENIX Association, 2008, pp. 209–224.C. Cadar, K. Sen, Symbolic execution for software testing: three decades later, Commun. ACM 56 (2) (Feb. 2013) 82–90.A. Cimatti, A. Griggio, Software model checking via IC3, in: 24th International Conference on Computer Aided Verification, in: Lect. Notes Comput. Sci., vol. 7358, Springer, 2012, pp. 277–293.M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, C.L. Talcott, All About Maude – A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, Lect. Notes Comput. Sci., vol. 4350, Springer, 2007.M. Clavel, J. Meseguer, M. Palomino, Reflection in membership equational logic, many-sorted equational logic, horn logic with equality, and rewriting logic, Theor. Comput. Sci. 373 (1–2) (2007) 70–91.G. Delzanno, A. Podelski, Constraint-based deductive model checking, Int. J. Softw. Tools Technol. Transf. 3 (3) (2001) 250–270.G. Dowek, C. Muñoz, C. Pas˘ areanu, ˘ A formal analysis framework for PLEXIL, in: 3rd Workshop on Planning and Plan Execution for Real-World Systems, September 2007, pp. 45–51.[23] G. Dowek, C. Muñoz, C. Pas˘ areanu, ˘ A Small-Step Semantics of PLEXIL, Technical Report 2008-11, National Institute of Aerospace, Hampton, VA, 2008.G. Dowek, C.A. Muñoz, C. Rocha, Rewriting logic semantics of a plan execution language, in: 6th Workshop on Structural Operational Semantics, in: Electron. Proc. Theor. Comput. Sci., vol. 18, 2009, pp. 77–91.F. Durán, S. Lucas, C. Marché, J. Meseguer, X. Urbain, Proving operational termination of membership equational programs, High.-Order Symb. Comput. 21 (1–2) (2008) 59–88.T. Estlin, A. Jónsson, C. Pas˘ areanu, ˘ R. Simmons, K. Tso, V. Verma, Plan Execution Interchange Language (PLEXIL), Technical Memorandum TM-2006-213483, NASA, 2006.S. Falke, D. Kapur, Dependency pairs for rewriting with built-in numbers and semantic data structures, in: 19th International Conference on Rewriting Techniques and Applications, in: Lect. Notes Comput. Sci., vol. 5117, Springer, Berlin, Heidelberg, 2008, pp. 94–109.S. Falke, D. Kapur, Operational termination of conditional rewriting with built-in numbers and semantic data structures, Electron. Notes Theor. Comput. Sci. 237 (2009) 75–90.S. Falke, D. Kapur, Rewriting induction + linear arithmetic = decision procedure, in: 6th International Joint Conference on Automated Reasoning, in: Lect. Notes Comput. Sci., vol. 7364, Springer, 2012, pp. 241–255.M. Ganai, A. Gupta, Accelerating high-level bounded model checking, in: 2006 IEEE/ACM International Conference on Computer Aided Design, Nov. 2006, pp. 794–801.H. Ganzinger, R. Nieuwenhuis, Constraints and theorem proving, in: Constraints in Computational Logics: Theory and Applications, International Sum mer School, in: Lect. Notes Comput. Sci., vol. 2002, Springer, 1999, pp. 159–201.T. Genet, T. Le Gall, A. Legay, V. Murat, A completion algorithm for lattice tree automata, in: 18th International Conference on Implementation and Application of Automata, in: Lect. Notes Comput. Sci., vol. 7982, Springer, 2013, pp. 134–145.S. Ghilardi, E. Nicolini, S. Ranise, D. Zucchelli, Combination methods for satisfiability and model-checking of infinite-state systems, in: 21st International Conference on Automated Deduction, in: Lect. Notes Comput. Sci., vol. 4603, Springer, 2007, pp. 362–378.S. Ghilardi, E. Nicolini, S. Ranise, D. Zucchelli, Towards SMT model checking of array-based systems, in: 4th International Joint Conference on Automated Reasoning, in: Lect. Notes Comput. Sci., vol. 5195, Springer, 2008, pp. 67–82.S. Ghilardi, S. Ranise, MCMT: a model checker modulo theories, in: 5th International Joint Conference on Automated Reasoning, in: Lect. Notes Comput. Sci., vol. 6173, Springer, 2010, pp. 22–29.J.A. Goguen, J. Meseguer, Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations, Theor. Comput. Sci. 105 (2) (1992) 217–273.H. Hojjat, P. Rümmer, P. Subotic, W. Yi, Horn clauses for communicating timed systems, in: N. Bjørner, F. Fioravanti, A. Rybalchenko, V. Senni (Eds.), 1st Workshop on Horn Clauses for Verification and Synthesis, in: Electron. Proc. Theor. Comput. Sci., vol. 169, 2014, pp. 39–52.H. Kirchner, C. Ringeissen, Combining symbolic constraint solvers on algebraic domains, J. Symb. Comput. 18 (2) (1994) 113–155.K. Kirchner, H. Kirchner, M. Rusinowitch, Deduction with symbolic constraints, Rev. Intell. Artif. 4 (3) (1990) 9–52.C. Kop, N. Nishida, Term rewriting with logical constraints, in: 9th International Symposium on Frontiers of Combining Systems, in: Lect. Notes Comput. Sci., vol. 8152, Springer, 2013, pp. 343–358.C. Kop, N. Nishida, Automatic constrained rewriting induction towards verifying procedural programs, in: 12th Asian Symposium on Programming Languages and Systems, in: Lect. Notes Comput. Sci., vol. 8858, Springer, 2014, pp. 334–353.[42] A. Lal, S. Qadeer, S. Lahiri, Corral: A Solver for Reachability Modulo Theories, Technical Report MSR-TR-2012-9, Microsoft Research, January 2012.K.G. Larsen, P. Pettersson, W. Yi, UPPAAL in a nutshell, Int. J. Softw. Tools Technol. Transf. 1 (1–2) (1997) 134–152.D. Lucanu, T.-F. Serbanuta, G. Rosu, K framework distilled, in: 9th International Workshop on Rewriting Logic and Its Applications, in: Lect. Notes Comput. Sci., vol. 7571, Springer, 2012, pp. 31–53.S. Lucas, J. Meseguer, Operational termination of membership equational programs: the order-sorted way, Electron. Notes Theor. Comput. Sci. 238 (3) (2009) 207–225.J. Meseguer, Conditional rewriting logic as a unified model of concurrency, Theor. Comput. Sci. 96 (1) (1992) 73–155.J. Meseguer, Membership algebra as a logical framework for equational specification, in: 12th International Workshop on Recent Trends in Algebraic Development Techniques, in: Lect. Notes Comput. Sci., vol. 1376, Springer, 1997, pp. 18–61.J. Meseguer, P. Thati, Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols, High.-Order Symb. Comput. 20 (1–2) (2007) 123–160.A. Milicevic, H. Kugler, Model checking using SMT and theory of lists, in: NASA 3rd International Symposium on Formal Methods, in: Lect. Notes Comput. Sci., vol. 6617, Springer, 2011, pp. 282–297.G. Nelson, D.C. Oppen, Simplification by cooperating decision procedures, ACM Trans. Program. Lang. Syst. 1 (2) (1979) 245–257.R. Nieuwenhuis, A. Oliveras, C. Tinelli, Solving SAT and SAT modulo theories: from an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T ), J. ACM 53 (6) (2006) 937–977.P.C. Ölveczky, M. Caccamo, Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude, in: L. Baresi, R. Heckel (Eds.), 9th International Conference on Fundamental Approaches to Software Engineering, in: Lect. Notes Comput. Sci., vol. 3922, Springer, 2006, pp. 357–372.S. Owre, J. Rushby, N. Shankar, PVS: a prototype verification system, in: 11th International Conference on Automated Deduction, in: Lect. Notes Artif. Intell., vol. 607, Springer-Verlag, Saratoga, NY, June 1992, pp. 748–752.A. Podelski, Model checking as constraint solving, in: 7th International Symposium on Static Analysis, in: Lect. Notes Comput. Sci., vol. 1824, Springer, 2000, pp. 22–37.C. Rocha, Symbolic Reachability Analysis for Rewrite Theories, PhD thesis, University of Illinois at Urbana-Champaign, 2012.C. Rocha, H. Cadavid, C.A. Muñoz, R. Siminiceanu, A formal interactive verification environment for the Plan Execution Interchange Language, in: 9th International Conference on Integrated Formal Methods, in: Lect. Notes Comput. Sci., vol. 7321, Springer, 2012, pp. 343–357.C. Rocha, J. Meseguer, C. Muñoz, Rewriting Modulo SMT, Technical Memorandum NASA/TM-2013-218033, NASA Langley Research Center, Hampton, VA, August 2013.C. Rocha, J. Meseguer, C. Muñoz, Rewriting modulo SMT and open system analysis, in: 10th International Workshop on Rewriting Logic and Its Appli cations, in: Lect. Notes Comput. Sci., vol. 8663, Springer International Publishing, 2014, pp. 247–262G. Ro ¸su, A. Stef ¸ anescu, ˘ Matching logic: a new program verification approach, in: 33rd International Conference on Software Engineering, ACM, New York, NY, USA, 2011, pp. 868–871.T. Rybina, A. Voronkov, A logical reconstruction of reachability, in: 5th International Andrei Ershov Memorial Conference on Perspectives of Systems Informatics, in: Lect. Notes Comput. Sci., vol. 2890, Springer, 2003, pp. 222–237.T. Sakata, N. Nishida, T. Sakabe, On proving termination of constrained term rewrite systems by eliminating edges from dependency graphs, in: 20th International Workshop on Functional and Constraint Logic Programming, in: Lect. Notes Comput. Sci., vol. 6816, Springer, 2011, pp. 138–155.P. Thati, J. Meseguer, Complete symbolic reachability analysis using back-and-forth narrowing, Theor. Comput. Sci. 366 (1–2) (2006) 163–179.M. Veanes, N. Bjørner, A. Raschke, An SMT approach to bounded reachability analysis of model programs, in: 28th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems, Springer, 2008, pp. 53–68.G. Vidal, Closed symbolic execution for verifying program termination, in: IEEE 12th International Working Conference on Source Code Analysis and Manipulation, Sept 2012, pp. 34–43.G. Vidal, Symbolic execution as a basis for termination analysis, Sci. Comput. Program. 102 (2015) 142–157P. Viry, Equational rules for rewriting logic, Theor. Comput. Sci. 285 (2002) 487–517.D. Walter, S. Little, C. Myers, Bounded model checking of analog and mixed-signal circuits using an SMT solver, in: 5th International Symposium on Automated Technology for Verification and Analysis, Springer, Berlin, Heidelberg, 2007, pp. 66–81.S. Yovine, KRONOS: a verification tool for real-time systems, Int. J. Softw. Tools Technol. Transf. 1 (1) (1997) 123–133Relaciones de conjuntos sincrónicosSemántica síncronaReescritura de lógicaSimulación formal y verificaciónSynchronous set relationsSynchronous semanticsRewriting logicFormal simulation and verificationPLEXILORIGINALRewriting modulo SMT and open system analysis.pdfRewriting modulo SMT and open system analysis.pdfArtículo principal.application/pdf827249https://repositorio.escuelaing.edu.co/bitstream/001/1866/1/Rewriting%20modulo%20SMT%20and%20open%20system%20analysis.pdfcc4ae003726dfd863f39bb4e5d6935f5MD51metadata only accessLICENSElicense.txtlicense.txttext/plain; charset=utf-81881https://repositorio.escuelaing.edu.co/bitstream/001/1866/2/license.txt5a7ca94c2e5326ee169f979d71d0f06eMD52open accessTEXTRewriting modulo SMT and open system analysis.pdf.txtRewriting modulo SMT and open system analysis.pdf.txtExtracted texttext/plain142253https://repositorio.escuelaing.edu.co/bitstream/001/1866/3/Rewriting%20modulo%20SMT%20and%20open%20system%20analysis.pdf.txtd1d03a6aa8d96400131fa8abe6cb763fMD53open accessTHUMBNAILRewriting modulo SMT and open system analysis.pdf.jpgRewriting modulo SMT and open system analysis.pdf.jpgGenerated Thumbnailimage/jpeg14815https://repositorio.escuelaing.edu.co/bitstream/001/1866/4/Rewriting%20modulo%20SMT%20and%20open%20system%20analysis.pdf.jpg60b583e806acbcefb9b4cde7a889fb31MD54open access001/1866oai:repositorio.escuelaing.edu.co:001/18662022-07-18 11:21:05.252metadata only accessRepositorio Escuela Colombiana de Ingeniería Julio Garavitorepositorio.eci@escuelaing.edu.coU0kgVVNURUQgSEFDRSBQQVJURSBERUwgR1JVUE8gREUgUEFSRVMgRVZBTFVBRE9SRVMgREUgTEEgQ09MRUNDScOTTiAiUEVFUiBSRVZJRVciLCBPTUlUQSBFU1RBIExJQ0VOQ0lBLgoKQXV0b3Jpem8gYSBsYSBFc2N1ZWxhIENvbG9tYmlhbmEgZGUgSW5nZW5pZXLDrWEgSnVsaW8gR2FyYXZpdG8gcGFyYSBwdWJsaWNhciBlbCB0cmFiYWpvIGRlIGdyYWRvLCBhcnTDrWN1bG8sIHZpZGVvLCAKY29uZmVyZW5jaWEsIGxpYnJvLCBpbWFnZW4sIGZvdG9ncmFmw61hLCBhdWRpbywgcHJlc2VudGFjacOzbiB1IG90cm8gKGVuICAgIGFkZWxhbnRlIGRvY3VtZW50bykgcXVlIGVuIGxhIGZlY2hhIAplbnRyZWdvIGVuIGZvcm1hdG8gZGlnaXRhbCwgeSBsZSBwZXJtaXRvIGRlIGZvcm1hIGluZGVmaW5pZGEgcXVlIGxvIHB1YmxpcXVlIGVuIGVsIHJlcG9zaXRvcmlvIGluc3RpdHVjaW9uYWwsIAplbiBsb3MgdMOpcm1pbm9zIGVzdGFibGVjaWRvcyBlbiBsYSBMZXkgMjMgZGUgMTk4MiwgbGEgTGV5IDQ0IGRlIDE5OTMsIHkgZGVtw6FzIGxleWVzIHkganVyaXNwcnVkZW5jaWEgdmlnZW50ZQphbCByZXNwZWN0bywgcGFyYSBmaW5lcyBlZHVjYXRpdm9zIHkgbm8gbHVjcmF0aXZvcy4gRXN0YSBhdXRvcml6YWNpw7NuIGVzIHbDoWxpZGEgcGFyYSBsYXMgZmFjdWx0YWRlcyB5IGRlcmVjaG9zIGRlIAp1c28gc29icmUgbGEgb2JyYSBlbiBmb3JtYXRvIGRpZ2l0YWwsIGVsZWN0csOzbmljbywgdmlydHVhbDsgeSBwYXJhIHVzb3MgZW4gcmVkZXMsIGludGVybmV0LCBleHRyYW5ldCwgeSBjdWFscXVpZXIgCmZvcm1hdG8gbyBtZWRpbyBjb25vY2lkbyBvIHBvciBjb25vY2VyLgpFbiBtaSBjYWxpZGFkIGRlIGF1dG9yLCBleHByZXNvIHF1ZSBlbCBkb2N1bWVudG8gb2JqZXRvIGRlIGxhIHByZXNlbnRlIGF1dG9yaXphY2nDs24gZXMgb3JpZ2luYWwgeSBsbyBlbGFib3LDqSBzaW4gCnF1ZWJyYW50YXIgbmkgc3VwbGFudGFyIGxvcyBkZXJlY2hvcyBkZSBhdXRvciBkZSB0ZXJjZXJvcy4gUG9yIGxvIHRhbnRvLCBlcyBkZSBtaSBleGNsdXNpdmEgYXV0b3LDrWEgeSwgZW4gY29uc2VjdWVuY2lhLCAKdGVuZ28gbGEgdGl0dWxhcmlkYWQgc29icmUgw6lsLiBFbiBjYXNvIGRlIHF1ZWphIG8gYWNjacOzbiBwb3IgcGFydGUgZGUgdW4gdGVyY2VybyByZWZlcmVudGUgYSBsb3MgZGVyZWNob3MgZGUgYXV0b3Igc29icmUgCmVsIGRvY3VtZW50byBlbiBjdWVzdGnDs24sIGFzdW1pcsOpIGxhIHJlc3BvbnNhYmlsaWRhZCB0b3RhbCB5IHNhbGRyw6kgZW4gZGVmZW5zYSBkZSBsb3MgZGVyZWNob3MgYXF1w60gYXV0b3JpemFkb3MuIEVzdG8gCnNpZ25pZmljYSBxdWUsIHBhcmEgdG9kb3MgbG9zIGVmZWN0b3MsIGxhIEVzY3VlbGEgYWN0w7phIGNvbW8gdW4gdGVyY2VybyBkZSBidWVuYSBmZS4KVG9kYSBwZXJzb25hIHF1ZSBjb25zdWx0ZSBlbCBSZXBvc2l0b3JpbyBJbnN0aXR1Y2lvbmFsIGRlIGxhIEVzY3VlbGEsIGVsIENhdMOhbG9nbyBlbiBsw61uZWEgdSBvdHJvIG1lZGlvIGVsZWN0csOzbmljbywgCnBvZHLDoSBjb3BpYXIgYXBhcnRlcyBkZWwgdGV4dG8sIGNvbiBlbCBjb21wcm9taXNvIGRlIGNpdGFyIHNpZW1wcmUgbGEgZnVlbnRlLCBsYSBjdWFsIGluY2x1eWUgZWwgdMOtdHVsbyBkZWwgdHJhYmFqbyB5IGVsIAphdXRvci5Fc3RhIGF1dG9yaXphY2nDs24gbm8gaW1wbGljYSByZW51bmNpYSBhIGxhIGZhY3VsdGFkIHF1ZSB0ZW5nbyBkZSBwdWJsaWNhciB0b3RhbCBvIHBhcmNpYWxtZW50ZSBsYSBvYnJhIGVuIG90cm9zIAptZWRpb3MuRXN0YSBhdXRvcml6YWNpw7NuIGVzdMOhIHJlc3BhbGRhZGEgcG9yIGxhcyBmaXJtYXMgZGVsIChsb3MpIGF1dG9yKGVzKSBkZWwgZG9jdW1lbnRvLiAKU8OtIGF1dG9yaXpvIChhbWJvcykK

Publicaciones similares