publications: - title: "Operational Semantics of the Marte Repetitive Structure Modeling Concepts for Data-Parallel Applications Design" author: - name: "Abdoulaye Gamatié" link: "https://researchr.org/alias/abdoulaye-gamati%C3%A9" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Éric Rutten" link: "https://researchr.org/alias/%C3%A9ric-rutten" year: "2010" doi: "http://doi.ieeecomputersociety.org/10.1109/ISPDC.2010.30" abstract: "This paper presents an operational semantics of the repetitive model of computation, which is the basis for the repetitive structure modeling (RSM) package defined in the standard UML Marte profile. It also deals with the semantics of an RSM extension for control-oriented design. The goal of this semantics is to serve as a formal support for i) reasoning about the behavioral properties of models specified in Marte with RSM, and ii) defining correct-by-construction model transformations for the production of executable code in a model-driven engineering framework. Available at http://hal.inria.fr/docs/00/52/27/87/PDF/gamatie_ispdc10.pdf" links: doi: "http://doi.ieeecomputersociety.org/10.1109/ISPDC.2010.30" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ispdc/GamatieRR10" tags: - "model-to-model transformation" - "semantics" - "transformation engineering" - "application framework" - "formal semantics" - "meta-model" - "modeling" - "UML" - "source-to-source" - "model-driven engineering" - "model transformation" - "operational semantics" - "Meta-Environment" - "design" - "transformation" researchr: "https://researchr.org/publication/GamatieRR10" cites: 0 citedby: 0 pages: "25-32" booktitle: "ispdc" kind: "inproceedings" key: "GamatieRR10" - title: "Embedding domain-specific modelling languages in maude specifications" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2011" month: "January" doi: "http://doi.acm.org/10.1145/1921532.1921557" abstract: "We propose an approach for embedding Domain-Specific Modelling Languages (DSML) into Maude, based on representing models and metamodels as Maude specifications, and on representing operational semantics and model transformations as computable functions/relations between such specifications. This provides us, on the one hand, with abstract definitions of essential concepts of domain-specific modelling languages: model-to-metamodel conformance, operational semantics, and (operational-semanticspreserving) model transformations; and, on the other hand, with equivalent executable definitions for those concepts, which can be directly used in Maude for formal verification purposes. PDF of extended version (accepted with minor changes in the Software and Systems modelling journal): http://chercheurs.lille.inria.fr/~rusu/SoSym/paper.pdf " links: doi: "http://doi.acm.org/10.1145/1921532.1921557" "url": "http://doi.acm.org/10.1145/1921532.1921557" tags: - "model-to-model transformation" - "semantics" - "rule-based" - "formal semantics" - "meta-model" - "modeling language" - "embedded software" - "modeling" - "transformation language" - "language modeling" - "source-to-source" - "transformation system" - "model transformation" - "operational semantics" - "Meta-Environment" - "systematic-approach" - "transformation" - "domain-specific language" researchr: "https://researchr.org/publication/Rusu%3A2011%3AEDM%3A1921532.1921557" cites: 0 citedby: 0 journal: "ACM SIGSOFT Software Engineering Notes" volume: "36" number: "1" pages: "1-8" kind: "article" key: "Rusu:2011:EDM:1921532.1921557" - title: "An Approach to Symbolic Test Generation" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Lydie du Bousquet" link: "https://researchr.org/alias/lydie-du-bousquet" - name: "Thierry Jéron" link: "https://researchr.org/alias/thierry-j%C3%A9ron" year: "2000" abstract: "Test generation is a program-synthesis problem: starting from the formal specification of a system under test, and from a test purpose describing a set of behaviours to be tested, compute a reactive program that observes an implementation of the system to detect non-conformant behaviour, while trying to control it towards satisfying the test purpose. In this paper we describe an approach for generating symbolic test cases, in the form of input-output automata with variables and parameters. " links: published: "https://researchr.org/publication/RusuBJ00" researchr: "https://researchr.org/publication/preprint-RusuBJ00" cites: 0 citedby: 0 type: "Preprint" kind: "techreport" key: "preprint-RusuBJ00" - title: "Verification Using Test Generation Techniques" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2002" links: published: "https://researchr.org/publication/Rusu02" researchr: "https://researchr.org/publication/preprint-Rusu02" cites: 0 citedby: 0 type: "Preprint" kind: "techreport" key: "preprint-Rusu02" - title: "Verification Using Test Generation Techniques" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2002" doi: "http://link.springer.de/link/service/series/0558/bibs/2391/23910252.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/2391/23910252.htm" technicalreport: "https://researchr.org/publication/preprint-Rusu02" tags: - "testing" researchr: "https://researchr.org/publication/Rusu02" cites: 0 citedby: 0 pages: "252-271" booktitle: "FM" kind: "inproceedings" key: "Rusu02" - title: "Analyzing Automata with Presburger Arithmetic and Uninterpreted Function Symbols" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Elena Zinovieva" link: "https://researchr.org/alias/elena-zinovieva" year: "2001" doi: "http://www.elsevier.com/gej-ng/31/29/23/85/30/show/Products/notes/index.htt#002" links: doi: "http://www.elsevier.com/gej-ng/31/29/23/85/30/show/Products/notes/index.htt#002" researchr: "https://researchr.org/publication/RusuZ01" cites: 0 citedby: 0 journal: "ENTCS" volume: "50" number: "4" pages: "327-341" kind: "article" key: "RusuZ01" - title: "From Safety Verification to Safety Testing" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Hervé Marchand" link: "https://researchr.org/alias/herv%C3%A9-marchand" - name: "Valéry Tschaen" link: "https://researchr.org/alias/val%C3%A9ry-tschaen" - name: "Thierry Jéron" link: "https://researchr.org/alias/thierry-j%C3%A9ron" - name: "Bertrand Jeannet" link: "https://researchr.org/alias/bertrand-jeannet" year: "2004" doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2978&spage=160" abstract: "A methodology that combines verification and conformance testing for validating safety requirements of reactive systems is presented. The requirements are first automatically verifed on the systems specification. Then test cases are automatically derived from the specification and the requirements and executed on a blackbox implementation of the system. The test cases attempt to push the implementation into violating a requirement. We show that an implementation conforms to its specification if and only if it passes all the test cases generated in this way Keywords verification conformance testing safety properties. Available at http://hal.inria.fr/docs/00/51/73/04/PDF/2004-TESTCOM.pdf" links: doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2978&spage=160" tags: - "testing" researchr: "https://researchr.org/publication/RusuMTJJ04" cites: 0 citedby: 0 pages: "160-176" booktitle: "TestCom 2004" kind: "inproceedings" key: "RusuMTJJ04" - title: "Embedding domain-specific modelling languages in Maude specifications" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2013" doi: "http://dx.doi.org/10.1007/s10270-012-0232-5" abstract: "We propose a formal approach for the definition and analysis of domain-specific modelling languages (DSML). The approach uses standard model-driven engineering artifacts for defining a language's syntax (using metamodels) and its operational semantics (using model transformations). We give formal meanings to these artifacts by translating them to the Maude language: metamodels and models are mapped to equational specifications, and model transformations are mapped to rewrite rules between such specifications, which are also expressible in Maude thanks to Maude's reflective capabilities. These mappings provide us, on the one hand, with abstract definitions of the MDE concepts used for defining DSML, which naturally capture their intended meanings; and, on the other hand, with equivalent executable definitions, which can be directly used by Maude for formal verification. We also study a notion of operational semantics-preserving model transformations, which are model transformations between two DSML that ensure that each execution of a transformed instance is matched by an execution of the original instance. We propose a semidecision procedure, implemented in Maude, for checking the semantics-preservation property. We also show how the procedure can be adapted for tracing finite executions of the transformed instance back to matching executions of the original one. The approach is illustrated on xSPEM, a language for describing the execution of activities constrained by time, precedence, and resource availability. Available at http://hal.inria.fr/hal-00660104." links: doi: "http://dx.doi.org/10.1007/s10270-012-0232-5" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/sosym/Rusu13" technicalreport: "https://researchr.org/publication/preprint-Rusu13" researchr: "https://researchr.org/publication/Rusu13" cites: 0 citedby: 0 journal: "SoSyM" volume: "12" number: "4" pages: "847-869" kind: "article" key: "Rusu13" - title: "Equational approximations for tree automata completion" author: - name: "Thomas Genet" link: "https://researchr.org/alias/thomas-genet" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2010" doi: "http://dx.doi.org/10.1016/j.jsc.2010.01.009" abstract: "In this paper we deal with the verification of safety properties of infinite-state systems modeled by term rewriting systems. An over-approximation of the set of reachable terms of a term rewriting system image is obtained by automatically constructing a finite tree automaton. The construction is parameterized by a set E of equations on terms, and we also show that the approximating automata recognize at most the set of image-reachable terms. Finally, we present some experiments carried out with the implementation of our algorithm. In particular, we show how some approximations from the literature can be defined using equational approximations. Available at http://hal.inria.fr/docs/00/49/54/05/PDF/genet-rusu-JSC-SCSS.pdf" links: doi: "http://dx.doi.org/10.1016/j.jsc.2010.01.009" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jsc/GenetR10" tags: - "meta-model" - "term rewriting" - "graph-rewriting" - "e-science" - "Meta-Environment" - "rewriting" researchr: "https://researchr.org/publication/GenetR10" cites: 0 citedby: 0 journal: "JSC" volume: "45" number: "5" pages: "574-597" kind: "article" key: "GenetR10" - title: "STG: a tool for generating symbolic test programs and oracles from operational specifications" author: - name: "Duncan Clarke" link: "https://researchr.org/alias/duncan-clarke" - name: "Thierry Jéron" link: "https://researchr.org/alias/thierry-j%C3%A9ron" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Elena Zinovieva" link: "https://researchr.org/alias/elena-zinovieva" year: "2001" doi: "http://doi.acm.org/10.1145/503209.503252" links: doi: "http://doi.acm.org/10.1145/503209.503252" tags: - "testing" researchr: "https://researchr.org/publication/ClarkeJRZ01%3A0" cites: 0 citedby: 0 pages: "301-302" booktitle: "ESEC/FSE" kind: "inproceedings" key: "ClarkeJRZ01:0" - title: "Symbolic Test Selection Based on Approximate Analysis" author: - name: "Bertrand Jeannet" link: "https://researchr.org/alias/bertrand-jeannet" - name: "Thierry Jéron" link: "https://researchr.org/alias/thierry-j%C3%A9ron" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Elena Zinovieva" link: "https://researchr.org/alias/elena-zinovieva" year: "2005" doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3440&spage=349" abstract: "This paper addresses the problem of generating symbolic test cases for testing the conformance of a black-box implementation with respect to a specification, in the context of reactive systems. The challenge we consider is the selection of test cases according to a test purpose, which is here a set of scenarii of interest that one wants to observe during test execution. Because of the interactions that occur between the test case and the implementation, test execution can be seen as a game involving two players, in which the test case attempts to satisfy the test purpose. Efficient solutions to this problem have been proposed in the context of finite-state models, based on the use of fixpoint computations. We extend them in the context of infinite-state symbolic models, by showing how approximate fixpoint computations can be used in a conservative way. The second contribution we provide is the formalization of a quality criterium for test cases, and a result relating the quality of a generated test case to the approximations used in the selection algorithm. Available at http://hal.inria.fr/docs/00/56/46/17/PDF/tacas05.pdf" links: doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3440&spage=349" tags: - "rule-based" - "meta-model" - "testing" - "analysis" - "context-aware" - "Meta-Environment" researchr: "https://researchr.org/publication/JeannetJRZ05" cites: 0 citedby: 0 pages: "349-364" booktitle: "TACAS" kind: "inproceedings" key: "JeannetJRZ05" - title: "Integrating formal verification and conformance testing for reactive systems" author: - name: "Camille Constant" link: "https://researchr.org/alias/camille-constant" - name: "Thierry Jéron" link: "https://researchr.org/alias/thierry-j%C3%A9ron" - name: "Hervé Marchand" link: "https://researchr.org/alias/herv%C3%A9-marchand" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2007" doi: "http://doi.ieeecomputersociety.org/10.1109/TSE.2007.70707" abstract: "In this paper, we describe a methodology integrating verification and conformance testing. A specification of a system— an extended input-output automaton, which may be infinite-state—and a set of safety properties (“nothing bad ever happens”) and possibility properties (“something good may happen”) are assumed. The properties are first tentatively verified on the specification using automatic techniques based on approximated state-space exploration, which are sound, but, as a price to pay for automation, are not complete for the given class of properties. Because of this incompleteness and of state-space explosion, the verification may not succeed in proving or disproving the properties. However, even if verification did not succeed, the testing phase can proceed and provide useful information about the implementation. Test cases are automatically and symbolically generated from the specification and the properties and are executed on a black-box implementation of the system. The test execution may detect violations of conformance between implementation and specification; in addition, it may detect violation/satisfaction of the properties by the implementation and by the specification. In this sense, testing completes verification. The approach is illustrated on simple examples and on a Bounded Retransmission Protocol. Available at http://hal.inria.fr/docs/00/42/29/04/PDF/2007-IEEE-TSE.pdf" links: doi: "http://doi.ieeecomputersociety.org/10.1109/TSE.2007.70707" tags: - "rule-based" - "completeness" - "protocol" - "testing" - "systematic-approach" researchr: "https://researchr.org/publication/ConstantJMR07" cites: 0 citedby: 0 journal: "TSE" volume: "33" number: "8" pages: "558-574" kind: "article" key: "ConstantJMR07" - title: "Formal executable semantics for conformance in the MDE framework" author: - name: "Marina Egea" link: "https://researchr.org/alias/marina-egea" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2010" doi: "http://dx.doi.org/10.1007/s11334-009-0108-1" abstract: "In the MDE framework, a metamodel is a language referring to some kind of metadata whose elements formalize concepts and relations providing a modeling language. An instance of this modeling language which adheres to its concepts and relations is called a valid model, i.e., a model satisfying structural conformance to its metamodel. However, a metamodel frequently imposes additional constraints to its valid instances. These conditions are usually written in OCL and are called well-formedness rules. In presence of these constraints, a valid model must adhere to the concepts and relations of its metamodel and fullfill its constraints, i.e., a valid model is a model satisfying semantical conformance to its metamodel. In this work, we provide a formal semantics to the notions of structural and semantical conformance between models and metamodels building on our previous work. Our definitions can be automatically checked using the ITP/OCL tool. Available at http://hal.inria.fr/docs/00/52/75/02/PDF/paper-IEEE.pdf" links: doi: "http://dx.doi.org/10.1007/s11334-009-0108-1" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/isse/EgeaR10" tags: - "semantics" - "OCL" - "rule-based" - "formal semantics" - "meta-model" - "modeling language" - "modeling" - "language modeling" - "constraints" - "rules" - "Meta-Environment" - "MDE" researchr: "https://researchr.org/publication/EgeaR10" cites: 0 citedby: 0 journal: "isse" volume: "6" number: "1-2" pages: "73-81" kind: "article" key: "EgeaR10" - title: "Compositional Verification of an ATM Protocol" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2003" abstract: "Abstraction and compositionality are key ingredients for the successful verification of complex infinite-state systems. In this paper we present an approach based on these ingredients and on theorem proving for verifying communication protocols. The approach is implemented in PVS. We demonstrate it by verifying the data transfer function of the SSCOP protocol, at ATM protocol whose main requirement is to perform a reliable data transfer over an unreliable communication medium." links: published: "https://researchr.org/publication/Rusu03" researchr: "https://researchr.org/publication/preprint-Rusu03" cites: 0 citedby: 0 type: "Preprint" kind: "techreport" key: "preprint-Rusu03" - title: "Hybrid Verifications of Reactive Programs" author: - name: "Olivier Roux" link: "https://researchr.org/alias/olivier-roux" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Franck Cassez" link: "https://researchr.org/alias/franck-cassez" year: "1999" links: published: "https://researchr.org/publication/RouxRC99" researchr: "https://researchr.org/publication/preprint-RouxRC99" cites: 0 citedby: 0 type: "Preprint" kind: "techreport" key: "preprint-RouxRC99" - title: "Language Definitions as Rewrite Theories" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Lucanu, Dorel" link: "https://researchr.org/alias/lucanu%2C-dorel" - name: "Serbanuta, Traian Florin " link: "https://researchr.org/alias/serbanuta%2C-traian-florin" - name: "Arusoaie, Andrei" link: "https://researchr.org/alias/arusoaie%2C-andrei" - name: "Stefanescu, Andrei" link: "https://researchr.org/alias/stefanescu%2C-andrei" - name: "Grigore Rosu" link: "http://fsl.cs.uiuc.edu/~grosu/" year: "2015" abstract: "K is a formal framework for defining operational semantics of programming languages. The K-Maude compiler translates K language definitions to Maude rewrite theories. The compiler enables program execution by using the Maude rewrite engine withthe compiled definitions, and program analysis by using various Maude analysis tools.K supports symbolic execution in Maude by means of an automatic transformation of language definitions. The transformed definition is called the {\\em symbolic extension} of the original definition.In this paper we investigate the theoretical relationship between K language definitions and their Maude translations, between symbolic extensions of K definitions and their Maude translations, and how the relationship between K definitions and their symbolic extensions is reflected on their respective representations in Maude.In particular, the results show how analysis performed with Maude tools can be formally lifted up to the original language definitions. Preprint available in the right-hand side panel." links: published: "https://researchr.org/publication/rusu%3Ahal-01186005" researchr: "https://researchr.org/publication/preprint-rusu%3Ahal-01186005" cites: 0 citedby: 0 type: "Preprint" kind: "techreport" key: "preprint-rusu:hal-01186005" - title: "Vérification d'invariants pour des systèmes spécifiés en logique de réécriture" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Clavel, Manuel" link: "https://researchr.org/alias/clavel%2C-manuel" year: "2009" abstract: "We present an approach based on inductive theorem proving for verifying invari- ants of dynamic systems specified in rewriting logic, a formal specification language imple- mented in the Maude system. An invariant is a property that holds on all the states that are reachable from a given class of initial states. Our approach consists in encoding the semantic aspects that are relevant for our task (namely, verifying invariance properties of the specified systems) in membership equational logic, a sublogic of rewriting logic. The invariance prop- erties are then formalized over the encoded rewrite theories and are proved using an inductive theorem prover for membership equational logic also implemented in the Maude system using its reflective capabilities. We illustrate our approach by verifying mutual exclusion properties of a readers-writers system and of an n-process version of the Bakery algorithm." links: "url": "http://hal.inria.fr/inria-00564219" researchr: "https://researchr.org/publication/rusu%3Ainria-00564219" cites: 0 citedby: 0 journal: "Studia Informatica Universalis" volume: "7" number: "2" kind: "article" key: "rusu:inria-00564219" - title: "(Co)inductive Proof Systems for Compositional Proofs in Reachability Logic" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "David Nowak" link: "https://researchr.org/alias/david-nowak" year: "2020" abstract: " (pdf preprint available in the left panel) Reachability Logic is a formalism that can be used, among others, for expressing partial-correctness properties of transition systems. In this paper we present three proof systems for this formalism, all of which are sound and complete and inherit the coinductive nature of the logic. The proof systems differ, however, in several aspects. First, they use induction and coinduction in different proportions. The second aspect regards compositionality, broadly meaning their ability to prove simpler formulas on smaller systems and to reuse those formulas as lemmas for proving more complex formulas on larger systems. The third aspect is the difficulty of their soundness proofs. We show that the more induction a proof system uses, and the more specialised is its use of coinduction (with respect to our problem domain), the more compositional the proof system is, but the more difficult is its soundness proof. We present formalisations of these results in the Coq proof assistant. In particular we have developed support for coinductive proofs that is comparable to that provided by Coq for inductive proofs. This may be of interest to a broader class of Coq users." links: technicalreport: "https://researchr.org/publication/preprint-rn20" researchr: "https://researchr.org/publication/rn20" cites: 0 citedby: 0 journal: "Journal of Logical and Algebraic Methods in Programming" kind: "article" key: "rn20" - title: "Model-Based Test Selection for Infinite-State Reactive Systems" author: - name: "Bertrand Jeannet" link: "https://researchr.org/alias/bertrand-jeannet" - name: "Thierry Jéron" link: "https://researchr.org/alias/thierry-j%C3%A9ron" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2006" doi: "http://dx.doi.org/10.1007/978-3-540-74792-5_3" abstract: "This paper addresses the problem of off-line selection of test cases for testing the conformance of a black-box implementation with respect to a specification, in the context of reactive systems. Efficient solutions to this problem have been proposed in the context of finite-state models, based on the ioco conformance testing theory. An extension of these is proposed in the context of infinite-state specifications, modelled as automata extended with variables. One considers the selection of test cases according to test purposes describing abstract scenarios that one wants to test. The selection of program test cases then consists in syntactical transformations of the specification model, using approximate analyses. Available at http://hal.inria.fr/docs/00/56/46/04/PDF/fmco06.pdf" links: doi: "http://dx.doi.org/10.1007/978-3-540-74792-5_3" tags: - "model-to-model transformation" - "automata theory" - "rule-based" - "meta programming" - "reactive programming" - "meta-model" - "modeling" - "testing model transformations" - "testing" - "source-to-source" - "transformation system" - "model transformation" - "context-aware" - "Meta-Environment" - "transformation" - "program transformation" researchr: "https://researchr.org/publication/JeannetJR06" cites: 0 citedby: 0 pages: "47-69" booktitle: "FMCO" kind: "inproceedings" key: "JeannetJR06" - title: "Verifying a Sliding Window Protocol using PVS" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2001" abstract: " We present the deductive verification of safety and liveness properties of a sliding-window protocol using the PVS theorem prover. The protocol is modeled in an operational style which is close to an actual program. It has parametric window sizes for both sender and receiver, and unbounded lossy communication channels carrying unbounded data. The proofs are done using invariant strengthening techniques encoded as PVS automated strategies based on heuristics and decision procedures." tags: - "rule-based" - "meta programming" - "program verification" - "meta-model" - "protocol" - "data-flow programming" - "data-flow" - "Meta-Environment" researchr: "https://researchr.org/publication/Rusu01" cites: 0 citedby: 0 pages: "251-268" booktitle: "forte" kind: "inproceedings" key: "Rusu01" - title: "Integrating Verification, Testing, and Learning for Cryptographic Protocols" author: - name: "Martijn Oostdijk" link: "https://researchr.org/alias/martijn-oostdijk" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Jan Tretmans" link: "https://researchr.org/alias/jan-tretmans" - name: "René G. de Vries" link: "https://researchr.org/alias/ren%C3%A9-g.-de-vries" - name: "Tim A. C. Willemse" link: "https://researchr.org/alias/tim-a.-c.-willemse" year: "2007" doi: "http://dx.doi.org/10.1007/978-3-540-73210-5_28" abstract: "The verification of cryptographic protocol specifications is an active research topic and has received much attention from the formal verification community. By contrast, the black-box testing of actual implementations of protocols, which is, arguably, as important as verification for ensuring the correct functioning of protocols in the “real” world, is little studied. We propose an approach for checking secrecy and authenticity properties not only on protocol specifications, but also on black-box implementations. The approach is compositional and integrates ideas from verification, testing, and learning. It is illustrated on the Basic Access Control protocol implemented in biometric passports. Available at http://hal.inria.fr/docs/00/56/42/31/PDF/2007-IFM.pdf" links: doi: "http://dx.doi.org/10.1007/978-3-540-73210-5_28" tags: - "protocol" - "composition" - "testing" - "C++" - "access control" - "systematic-approach" researchr: "https://researchr.org/publication/OostdijkRTVW07" cites: 0 citedby: 0 pages: "538-557" booktitle: "IFM" kind: "inproceedings" key: "OostdijkRTVW07" - title: "Verifying Reachability-Logic Properties on Rewriting-Logic Specifications" author: - name: "Andrei Arusoaie" link: "https://researchr.org/alias/andrei-arusoaie" - name: "Dorel Lucanu" link: "https://researchr.org/alias/dorel-lucanu" - name: "David Nowak" link: "https://researchr.org/alias/david-nowak" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2015" abstract: " Reachability Logic is a recently introduced formalism, which is currently used for defining the operational semantics of programming languages and for stating properties about program executions. In this paper we show how Reachability Logic can be adapted for stating prop- erties of transition systems described by Rewriting-Logic specifications. We propose an automatic procedure for verifying Rewriting-Logic speci- fications against Reachability-Logic properties. We prove the soundness of the procedure and illustrate it by verifying a communication protocol specified in Maude. Preprint PDF available on the left-hand side tab." links: published: "https://researchr.org/publication/ArusoaieLucanuNowakand-Vlad-Rusu2015-0" researchr: "https://researchr.org/publication/preprint-ArusoaieLucanuNowakand-Vlad-Rusu2015-0" cites: 0 citedby: 0 type: "Preprint" kind: "techreport" key: "preprint-ArusoaieLucanuNowakand-Vlad-Rusu2015-0" - title: "Compositional Verification of an ATM Protocol" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2003" doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2805&spage=223" abstract: "Abstraction and compositionality are key ingredients for the successful verification of complex infinite-state systems. In this paper we present an approach based on these ingredients and on theorem proving for verifying communication protocols. The approach is implemented in PVS. We demonstrate it by verifying the data transfer function of the SSCOP protocol, at ATM protocol whose main requirement is to perform a reliable data transfer over an unreliable communication medium." links: doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2805&spage=223" technicalreport: "https://researchr.org/publication/preprint-Rusu03" tags: - "rule-based" - "protocol" - "composition" - "data-flow" - "abstraction" - "systematic-approach" researchr: "https://researchr.org/publication/Rusu03" cites: 0 citedby: 0 pages: "223-243" booktitle: "FM" kind: "inproceedings" key: "Rusu03" - title: "Ensuring the conformance of reactive discrete-event systems by means of supervisory control" author: - name: "Jeron, T." link: "https://researchr.org/alias/jeron%2C-t." - name: "Marchand, H." link: "https://researchr.org/alias/marchand%2C-h." - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Tschaen, V." link: "https://researchr.org/alias/tschaen%2C-v." year: "2004" abstract: "We study the problem of controlling a plant of a system by means of an automatically computed supervisor, in order to ensure a certain conformance relation between the plant and its formal specification. The supervisor can be seen as a device that automatically fixes errors, which otherwise should have been discovered by testing and fixed by hand. The resulting controlled plant conforms to the specification and is maximal in terms of observable behavior. Available at http://hal.inria.fr/docs/00/52/76/69/PDF/2004-IJPR.pdf" tags: - "control systems" - "testing" researchr: "https://researchr.org/publication/jeron04a" cites: 0 citedby: 0 journal: "International Journal of Production Research" volume: "42" number: "14" kind: "article" key: "jeron04a" - title: "Towards a K Semantics for OCL" author: - name: "Andrei Arusoaie" link: "https://researchr.org/alias/andrei-arusoaie" - name: "Dorel Lucanu" link: "https://researchr.org/alias/dorel-lucanu" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2014" doi: "http://dx.doi.org/10.1016/j.entcs.2014.05.004" abstract: "We give a formal definition to a significant subset of the Object Constraint Language (OCL) in the K framework. The chosen subset includes the usual arithmetical, Boolean (including quantifiers), and string expressions; collection expressions (including iterators and navigation); and pre/post conditions for methods. Being executable, our definition provides us, for free, with an interpreter for the chosen subset of OCL. It can be used for free in K definitions of languages having OCL as a component We illustrate some of the advantages of K by comparing our semantical definition of OCL with the official semantics from the language’s standard. We also report on a tool implementing our definition that users can try online. PDF available at https://hal.inria.fr/hal-00998923/document" links: doi: "http://dx.doi.org/10.1016/j.entcs.2014.05.004" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/entcs/ArusoaieLR14" researchr: "https://researchr.org/publication/ArusoaieLR14" cites: 0 citedby: 0 journal: "ENTCS" volume: "304" pages: "81-96" kind: "article" key: "ArusoaieLR14" - title: "A language-independent proof system for full program equivalence" author: - name: "Stefan Ciobaca" link: "https://researchr.org/alias/stefan-ciobaca" - name: "Dorel Lucanu" link: "https://researchr.org/alias/dorel-lucanu" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Grigore Rosu" link: "https://researchr.org/alias/grigore-rosu" year: "2016" doi: "http://dx.doi.org/10.1007/s00165-016-0361-7" abstract: "Two programs are mutually equivalent if, for the same input, either they both diverge or they both terminate with the same result. Mutual equivalence is an adequate notion of equivalence for programs written in deterministic languages. It is useful in many contexts, such as capturing the correctness of program transformations within the same language, or capturing the correctness of compilers between two different languages. In this paper we introduce a language-independent proof system for mutual equivalence, which is para-metric in the operational semantics of two languages and in a state-similarity relation. The proof system is sound: if it terminates then it establishes the mutual equivalence of the programs given to it as input. We illustrate it on two programs in two different languages (an imperative one and a functional one), that both compute the Collatz sequence. The Collatz sequence is an interesting case study since it is not known wether the sequence terminates or not; nevertheless, our proof system shows that the two programs are mutually equivalent (even if we cannot establish termination or divergence of either one). PDF available at https://hal.inria.fr/hal-01245528." links: doi: "http://dx.doi.org/10.1007/s00165-016-0361-7" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/fac/CiobacaLRR16" researchr: "https://researchr.org/publication/CiobacaLRR16" cites: 0 citedby: 0 journal: "fac" volume: "28" number: "3" pages: "469-497" kind: "article" key: "CiobacaLRR16" - title: "Executing and verifying higher-order functional-imperative programs in Maude" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Andrei Arusoaie" link: "https://researchr.org/alias/andrei-arusoaie" year: "2017" doi: "https://doi.org/10.1016/j.jlamp.2017.09.002" abstract: "We incorporate higher-order functions and state monads in Maude, thereby embedding a higher-order functional language with imperative features in the Maude framework. We illustrate, via simple programs in the resulting language: the concrete and symbolic execution of programs; their verification with respect to properties expressed in Reachability Logic, a language-parametric generalisation of Hoare Logic; and the verification of program-equivalence properties. Our approach is proved sound and is implemented in Full Maude by taking advantage of its reflective features and module system. PDF available at https://hal.inria.fr/hal-01586341." links: doi: "https://doi.org/10.1016/j.jlamp.2017.09.002" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jlp/RusuA17" researchr: "https://researchr.org/publication/RusuA17-0" cites: 0 citedby: 0 journal: "jlp" volume: "93" pages: "68-91" kind: "article" key: "RusuA17-0" - title: "A generic framework for symbolic execution: A coinductive approach" author: - name: "Dorel Lucanu" link: "https://researchr.org/alias/dorel-lucanu" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Andrei Arusoaie" link: "https://researchr.org/alias/andrei-arusoaie" year: "2017" doi: "http://dx.doi.org/10.1016/j.jsc.2016.07.012" abstract: " We propose a language-independent symbolic execution framework. The approach is parameterised by a language definition, which consists of a signature for the lan-guage's syntax and execution infrastructure, a model interpreting the signature, and rewrite rules for the language's operational semantics. Then, symbolic execution amounts to computing symbolic paths using a derivative operation. We prove that the symbolic execution thus defined has the properties naturally expected from it, meaning that the feasible symbolic executions of a program and the concrete executions of the same program mutually simulate each other. We also show how a coinduction-based extension of symbolic execution can be used for the deductive verification of programs. We show how the proposed symbolic-execution approach, and the coinductive verification technique based on it, can be seamlessly implemented in language definition frameworks based on rewriting such as the K framework. A prototype implementation of our approach has been developed in K. We illustrate it on the symbolic analysis and deductive verification of nontrivial programs. PDF available at https://hal.inria.fr/hal-01238696." links: doi: "http://dx.doi.org/10.1016/j.jsc.2016.07.012" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jsc/LucanuRA17" researchr: "https://researchr.org/publication/LucanuRA17" cites: 0 citedby: 0 journal: "JSC" volume: "80" pages: "125-163" kind: "article" key: "LucanuRA17" - title: "Combining Theorem Proving and Narrowing for Rewriting-Logic Specifications" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2010" doi: "http://dx.doi.org/10.1007/978-3-642-13977-2_12" abstract: "We present an approach for verifying dynamic systems specified in rewriting logic, a formal specification language implemented in the Maude system. Our approach is tailored for invariants, i.e., properties that hold on all states reachable from a given class of initial states. The approach consists in encoding invariance properties into inductive properties written in membership equational logic, a sublogic of rewriting logic also implemented in Maude. The invariants can then be verified using an inductive theorem prover available for membership equational logic, possibly in interaction with narrowing-based symbolic analysis tools for rewriting-logic specifications also available in the Maude environment. We show that it is possible, and useful, to automatically test invariants by symbolic analysis before interactively proving them. Available at http://hal.inria.fr/docs/00/52/78/64/PDF/2010-tap.pdf" links: doi: "http://dx.doi.org/10.1007/978-3-642-13977-2_12" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/tap/Rusu10" tags: - "rule-based" - "testing" - "analysis" - "graph-rewriting" - "logic" - "Meta-Environment" - "rewriting logic" - "rewriting" - "systematic-approach" researchr: "https://researchr.org/publication/Rusu10" cites: 0 citedby: 0 pages: "135-150" booktitle: "tap" kind: "inproceedings" key: "Rusu10" - title: "Task-System Analysis Using Slope-Parametric Hybrid Automata" author: - name: "Augusto Burgueño" link: "https://researchr.org/alias/augusto-burgue%C3%B1o" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "1997" tags: - "analysis" researchr: "https://researchr.org/publication/BurguenoR97" cites: 0 citedby: 0 pages: "1262-1273" booktitle: "europar" kind: "inproceedings" key: "BurguenoR97" - title: "Verifying an ATM Protocol Using a Combination of Formal Techniques" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2006" doi: "http://dx.doi.org/10.1093/comjnl/bxl039" abstract: "This paper describes a methodology and a case study in formal verification. The case study is the SSCOP protocol, a member of the ATM adaptation layer whose main role is to perform a reliable data transfer over an unreliable communication medium. The methodology involves: (1) simulation for initial debugging; (2) partial-order abstraction that preserves the properties of interest; and (3) compositional verification of the properties at the abstract level using the PVS theorem prover. Steps (2) and (3) guarantee that the properties still hold on the whole (composed, concrete) system. The value of the approach lies in adapting and integrating several existing formal techniques into a new verification methodology that is able to deal with real case studies. Available at http://hal.inria.fr/docs/00/07/14/94/PDF/RR-5089.pdf as a research report." links: doi: "http://dx.doi.org/10.1093/comjnl/bxl039" tags: - "case study" - "protocol" - "composition" - "data-flow" - "debugging" - "abstraction" - "systematic-approach" researchr: "https://researchr.org/publication/Rusu06" cites: 0 citedby: 0 journal: "cj" volume: "49" number: "6" pages: "710-730" kind: "article" key: "Rusu06" - title: "Symbolic Determinisation of Extended Automata" author: - name: "Thierry Jéron" link: "https://researchr.org/alias/thierry-j%C3%A9ron" - name: "Hervé Marchand" link: "https://researchr.org/alias/herv%C3%A9-marchand" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2006" doi: "http://dx.doi.org/10.1007/978-0-387-34735-6_18" abstract: "We define a symbolic determinisation procedure for a class of infinite-state systems, which consists of automata extended with symbolic variables that may be infinite-state. The subclass of extended automata for which the procedure terminates is characterised as bounded lookahead extended automata. It corresponds to automata for which, in any location, the observation of a bounded-length trace is enough to infer the first transition actually taken. We discuss applications of the algorithm to the verification, testing, and diagnosis of infinite-state systems. Availablr at http://hal.inria.fr/docs/00/42/48/58/PDF/2006-TCS-Deter.pdf" links: doi: "http://dx.doi.org/10.1007/978-0-387-34735-6_18" tags: - "testing" researchr: "https://researchr.org/publication/JeronMR06" cites: 0 citedby: 0 pages: "197-212" booktitle: "ifipTCS" kind: "inproceedings" key: "JeronMR06" - title: "Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant" author: - name: "Gilles Barthe" link: "https://researchr.org/alias/gilles-barthe" - name: "Julien Forest" link: "https://researchr.org/alias/julien-forest" - name: "David Pichardie" link: "https://researchr.org/alias/david-pichardie" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2006" doi: "http://dx.doi.org/10.1007/11737414_9" abstract: "We present a practical tool for defining and proving properties of recursive functions in the Coq proof assistant. The tool proceeds by generating from pseudo-code (Coq functions that need not be total nor terminating) the graph of the intended function as an inductive relation, and then proves that the relation actually represents a function, which is by construction the function that we are trying to define. Then, we generate induction and inversion principles , and a fixpoint equation for proving other properties of the function. Our tool builds upon state-of-the-art techniques for defining recursive functions, and can also be used to generate executable functions from inductive descriptions of their graph. We illustrate the benefits of our tool on two case studies. Available at http://hal.inria.fr/docs/00/56/42/37/PDF/2006-FLOPS.pdf" links: doi: "http://dx.doi.org/10.1007/11737414_9" tags: - "proof assistant" - "case study" - "principles" - "equational proofs" - "graph-rewriting" - "rewriting" researchr: "https://researchr.org/publication/BartheFPR06" cites: 0 citedby: 0 pages: "114-129" booktitle: "FLOPS" kind: "inproceedings" key: "BartheFPR06" - title: "A Theoretical Foundation for Programming Languages Aggregation" author: - name: "Stefan Ciobaca" link: "https://researchr.org/alias/stefan-ciobaca" - name: "Dorel Lucanu" link: "https://researchr.org/alias/dorel-lucanu" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Grigore Rosu" link: "https://researchr.org/alias/grigore-rosu" year: "2014" doi: "http://dx.doi.org/10.1007/978-3-319-28114-8_3" links: doi: "http://dx.doi.org/10.1007/978-3-319-28114-8_3" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/wadt/CiobacaLRR14" researchr: "https://researchr.org/publication/CiobacaLRR14-0" cites: 0 citedby: 0 pages: "30-47" booktitle: "WADT" kind: "inproceedings" key: "CiobacaLRR14-0" - title: "Validation of Reactive Systems" author: - name: "Constant, C." link: "https://researchr.org/alias/constant%2C-c." - name: "Jeron, T." link: "https://researchr.org/alias/jeron%2C-t." - name: "Marchand, H." link: "https://researchr.org/alias/marchand%2C-h." - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2008" month: "January" tags: - "C++" researchr: "https://researchr.org/publication/book-chap-react-systems" cites: 0 citedby: 0 booktitle: "Modeling and Verification of Real-TIME Systems - Formalisms and software Tools" publisher: "Herm?s Science" kind: "incollection" key: "book-chap-react-systems" - title: "Verifying Reachability-Logic Properties on Rewriting-Logic Specifications" author: - name: "Dorel Lucanu" link: "https://researchr.org/alias/dorel-lucanu" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Andrei Arusoaie" link: "https://researchr.org/alias/andrei-arusoaie" - name: "David Nowak" link: "https://researchr.org/alias/david-nowak" year: "2015" abstract: " Reachability Logic is a recently introduced formalism, which is currently used for defining the operational semantics of programming languages and for stating properties about program executions. In this paper we show how Reachability Logic can be adapted for stating properties of transition systems described by Rewriting-Logic specifications. We propose an automatic procedure for verifying Rewriting-Logic specifications against Reachability-Logic properties. We prove the soundness of the procedure and illustrate it by verifying a communication protocol specified in Maude. PDF available at https://hal.inria.fr/hal-01158941." links: technicalreport: "https://researchr.org/publication/preprint-ArusoaieLucanuNowakand-Vlad-Rusu2015-0" researchr: "https://researchr.org/publication/ArusoaieLucanuNowakand-Vlad-Rusu2015-0" cites: 0 citedby: 0 booktitle: "Logic, Rewriting and Concurrency: Festschrift Symposium in Honor of José Meseguer" kind: "inproceedings" key: "ArusoaieLucanuNowakand-Vlad-Rusu2015-0" - title: "Hybrid Verifications of Reactive Programs" author: - name: "Olivier Roux" link: "https://researchr.org/alias/olivier-roux" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Franck Cassez" link: "https://researchr.org/alias/franck-cassez" year: "1999" doi: "http://link.springer.de/link/service/journals/00165/bibs/9011004/90110448.htm" links: doi: "http://link.springer.de/link/service/journals/00165/bibs/9011004/90110448.htm" technicalreport: "https://researchr.org/publication/preprint-RouxRC99" tags: - "reactive programming" - "program verification" - "programming" researchr: "https://researchr.org/publication/RouxRC99" cites: 0 citedby: 0 journal: "fac" volume: "11" number: "4" pages: "448-471" kind: "article" key: "RouxRC99" - title: "Program Equivalence by Circular Reasoning" author: - name: "Lucanu, Dorel" link: "https://researchr.org/alias/lucanu%2C-dorel" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2014" links: published: "https://researchr.org/publication/lucanu%3Ahal-01065830" researchr: "https://researchr.org/publication/preprint-lucanu%3Ahal-01065830" cites: 0 citedby: 0 type: "Preprint" kind: "techreport" key: "preprint-lucanu:hal-01065830" - title: "A Language-Independent Proof System for Mutual Program Equivalence" author: - name: "Stefan Ciobaca" link: "https://researchr.org/alias/stefan-ciobaca" - name: "Dorel Lucanu" link: "https://researchr.org/alias/dorel-lucanu" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Grigore Rosu" link: "http://fsl.cs.uiuc.edu/~grosu/" year: "2014" doi: "http://dx.doi.org/10.1007/978-3-319-11737-9_6" abstract: "Two programs are mutually equivalent if they both diverge or they end up in similar states. Mutual equivalence is an adequate notion of equivalence for programs written in deterministic languages. It is useful in many contexts, such as capturing the correctness of program transformations within the same language, or capturing the correctness of compilers between two different languages. In this paper we introduce a language-independent proof system for mutual equivalence, which is parametric in the operational semantics of two languages and in a statesimilarity relation. The proof system is sound: if it terminates then it establishes the mutual equivalence of the programs given to it as input. We illustrate it on two programs in two different languages (an imperative one and a functional one), that both compute the Collatz sequence. PDF available at https://hal.inria.fr/hal-01030754/document" links: doi: "http://dx.doi.org/10.1007/978-3-319-11737-9_6" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfem/CiobacaLRR14" researchr: "https://researchr.org/publication/CiobacaLRR14" cites: 0 citedby: 0 pages: "75-90" booktitle: "icfem" kind: "inproceedings" key: "CiobacaLRR14" - title: "A Generic Framework for Symbolic Execution" author: - name: "Andrei Arusoaie" link: "https://researchr.org/alias/andrei-arusoaie" - name: "Dorel Lucanu" link: "https://researchr.org/alias/dorel-lucanu" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2013" doi: "http://dx.doi.org/10.1007/978-3-319-02654-1_16" abstract: "We propose a generic, language-independent symbolic execution approach for languages endowed with a formal operational semantics based on term rewriting. Starting from the definition of a language L, a new definition Lsym is automatically generated, which has the same syntax, but whose semantics extends L's data domains with symbolic values and adapts the semantical rules of L to deal with the new domains. Then, the symbolic execution of Lprograms is the concrete execution of the corresponding Lsym programs, i.e., the application of the rewrite rules in the semantics of Lsym. We prove that the symbolic execution thus defined has the adequate properties normally expected from it, and illustrate the approach on a simple imperative language defined in the K framework. A prototype symbolic execution engine also written in K is presented. Available at http://hal.inria.fr/hal-00853588." links: doi: "http://dx.doi.org/10.1007/978-3-319-02654-1_16" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/sle/ArusoaieLR13" researchr: "https://researchr.org/publication/ArusoaieLR13" cites: 0 citedby: 0 pages: "281-301" booktitle: "SLE" kind: "inproceedings" key: "ArusoaieLR13" - title: "A theoretical foundation for programming languages aggregation" author: - name: "Stefan Ciobaca" link: "https://researchr.org/alias/stefan-ciobaca" - name: "Dorel Lucanu" link: "https://researchr.org/alias/dorel-lucanu" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Grigore Rosu" link: "http://fsl.cs.uiuc.edu/~grosu/" year: "2015" abstract: "Programming languages should be formally specified in or- der to reason about programs written in them. We show that, given two formally specified programming languages, it is possible to construct the formal semantics of an aggregated language, in which programs consist of pairs of programs from the initial languages. The construction is based on algebraic techniques and it can be used to reduce relational proper- ties (such as equivalence of programs) to reachability properties (in the aggregated language). Full text available at https://hal.inria.fr/hal-01076641." links: "url": "https://hal.inria.fr/hal-01076641" researchr: "https://researchr.org/publication/ciobaca%3Ahal-01076641" cites: 0 citedby: 0 pages: "30-47" booktitle: "22nd International Workshop on Algebraic Development Techniques" kind: "inproceedings" key: "ciobaca:hal-01076641" - title: "A K-Based Formal Framework for Domain-Specific Modelling Languages" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Dorel Lucanu" link: "https://researchr.org/alias/dorel-lucanu" year: "2011" doi: "http://dx.doi.org/10.1007/978-3-642-31762-0_14" abstract: "We propose a formal approach for the definition of domain-specific modelling languages (DSMLs). The approach uses basic Model-Driven Engineering artifacts for defining a DSML's syntax (using metamodels) and its operational semantics (using model transformations). We give formal meanings to these artifacts by mapping them to the K semantic framework. The mapping is implemented in the Rascal metaprogramming language. Since the resulting K definitions are executable, one obtains an execution engine for DSMLs and gains acces to K's formal analysis tools. We illustrate the approach on xSPEM, a language for describing the execution of tasks constrained by time, precedence, and resources. Available at http://hal.inria.fr/inria-00637099." links: doi: "http://dx.doi.org/10.1007/978-3-642-31762-0_14" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/foveoos/RusuL11" researchr: "https://researchr.org/publication/RusuL11" cites: 0 citedby: 0 pages: "214-231" booktitle: "foveoos" kind: "inproceedings" key: "RusuL11" - title: "Language Definitions as Rewrite Theories" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Dorel Lucanu" link: "https://researchr.org/alias/dorel-lucanu" - name: "Traian-Florin Serbanuta" link: "https://researchr.org/alias/traian-florin-serbanuta" - name: "Andrei Arusoaie" link: "https://researchr.org/alias/andrei-arusoaie" - name: "Andrei Stefanescu" link: "https://researchr.org/alias/andrei-stefanescu" - name: "Grigore Rosu" link: "http://fsl.cs.uiuc.edu/~grosu/" year: "2016" month: "January" abstract: "K is a formal framework for defining operational semantics of programming languages. The K-Maude compiler translates K language definitions to Maude rewrite theories. The compiler enables program execution by using the Maude rewrite engine withthe compiled definitions, and program analysis by using various Maude analysis tools.K supports symbolic execution in Maude by means of an automatic transformation of language definitions. The transformed definition is called the {\\em symbolic extension} of the original definition.In this paper we investigate the theoretical relationship between K language definitions and their Maude translations, between symbolic extensions of K definitions and their Maude translations, and how the relationship between K definitions and their symbolic extensions is reflected on their respective representations in Maude.In particular, the results show how analysis performed with Maude tools can be formally lifted up to the original language definitions. Preprint available at https://hal.inria.fr/hal-01186005." links: technicalreport: "https://researchr.org/publication/preprint-rusu%3Ahal-01186005" "url": "https://hal.inria.fr/hal-01186005" researchr: "https://researchr.org/publication/rusu%3Ahal-01186005" cites: 0 citedby: 0 journal: "jlamp" volume: "85" number: "1 Part 1" pages: "98-120" kind: "article" key: "rusu:hal-01186005" - title: "(Co)inductive Proof Systems for Compositional Proofs in Reachability Logic" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "David Nowak" link: "https://researchr.org/alias/david-nowak" year: "2019" doi: "10.4204/EPTCS.303.3" abstract: "Reachability Logic is a formalism that can be used, among others, for expressing partial-correctness properties of transition systems. In this paper we present three proof systems for this formalism, all of which are sound and complete and inherit the coinductive nature of the logic. The proof systems differ, however, in several aspects. First, they use induction and coinduction in different proportions. The second aspect regards compositionality, broadly meaning their ability to prove simpler formulas on smaller systems, and to reuse those formulas as lemmas for more complex formulas on larger systems. The third aspect is the difficulty of their soundness proofs. We show that the more induction a proof system uses, and the more specialised is its use of coinduction (with respect to our problem domain), the more compositional the proof system is, but the more difficult its soundness proof becomes. We also briefly present mechanisations of these results in the Isabelle/HOL and Coq proof assistants. Available athttps://hal.archives-ouvertes.fr/hal-02176456." links: "url": "https://doi.org/10.4204/EPTCS.303.3" researchr: "https://researchr.org/publication/DBLP%3Ajournals-corr-abs-1909-01744" cites: 0 citedby: 0 pages: "32-47" booktitle: "Proceedings Third Symposium on Working Formal Methods, Electronic Proceeding in Theoretical Computer Science 303" kind: "inproceedings" key: "DBLP:journals-corr-abs-1909-01744" - title: "Reachability Verification for Hybrid Automata" author: - name: "Thomas A. Henzinger" link: "https://researchr.org/alias/thomas-a.-henzinger" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "1998" researchr: "https://researchr.org/publication/HenzingerR98" cites: 0 citedby: 0 pages: "190-204" booktitle: "hybrid" kind: "inproceedings" key: "HenzingerR98" - title: "Translating from GRAFCET to the reactive language ELECTRE" author: - name: "Roux, O." link: "https://researchr.org/alias/roux%2C-o." - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "1994" tags: - "translation" researchr: "https://researchr.org/publication/roux94" cites: 0 citedby: 0 journal: "Automatique, Productique et Informatique Industrielle" volume: "28" number: "2" kind: "article" key: "roux94" - title: "Program Equivalence by Circular Reasoning" author: - name: "Dorel Lucanu" link: "https://researchr.org/alias/dorel-lucanu" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2013" doi: "http://dx.doi.org/10.1007/978-3-642-38613-8_25" abstract: "We propose a logic and a deductive system for stating and automatically proving the equivalence of programs in deterministic languages having a rewriting-based operational semantics. The deductive system is circular in nature and is proved sound and weakly complete; together, these results say that, when it terminates, our system correctly solves the program-equivalence problem as we state it. We show that our approach is suitable for proving the equivalence of both terminating and non-terminating programs, and also the equivalence of both concrete and symbolic programs. The latter are programs in which some statements or expressions are symbolic variables. By proving the equivalence between symbolic programs, one proves in one shot the equivalence of (possibly, infinitely) many concrete programs obtained by replacing the variables by concrete statements or expressions. We also report on a prototype implementation of the proposed deductive system in the K Framework. Available at http://hal.inria.fr/hal-00820871." links: doi: "http://dx.doi.org/10.1007/978-3-642-38613-8_25" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ifm/LucanuR13" researchr: "https://researchr.org/publication/LucanuR13" cites: 0 citedby: 0 pages: "362-377" booktitle: "IFM" kind: "inproceedings" key: "LucanuR13" - title: "Symbolic execution based on language transformation" author: - name: "Andrei Arusoaie" link: "https://researchr.org/alias/andrei-arusoaie" - name: "Dorel Lucanu" link: "https://researchr.org/alias/dorel-lucanu" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2015" doi: "http://dx.doi.org/10.1016/j.cl.2015.08.004" links: doi: "http://dx.doi.org/10.1016/j.cl.2015.08.004" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/cl/ArusoaieLR15" researchr: "https://researchr.org/publication/ArusoaieLR15" cites: 0 citedby: 0 journal: "Comp. Lang., Syst. \\& Struct." volume: "44" pages: "48-71" kind: "article" key: "ArusoaieLR15" - title: "Proving Partial-Correctness and Invariance Properties of Transition-System Models" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Gilles Grimaud" link: "https://researchr.org/alias/gilles-grimaud" - name: "Michaël Hauspie" link: "https://researchr.org/alias/micha%C3%ABl-hauspie" year: "2020" doi: "10.1016/j.scico.2019.102342" abstract: " We propose an approach for proving partial-correctness and invariance properties of transition systems, and illustrate it on a model of a security hypervisor. Regarding partial correctness, we generalise the recently introduced formalism of Reachability Logic, currently used as a language-parametric logic for programs, to transition systems. We propose a coinductive proof system for the resulting logic, which can be seen as performing an “infinite symbolic execution” of the transition-system model under verification. We embed the proof system in the Coq proof assistant and formally prove its soundness and completeness. The soundness result provides us with a Coq-certified Reachability-Logic prover for transition-system models. The completeness result, although more theoretical in nature, also has a practical value, as it suggests a proof strategy that is able to deal with all valid formulas on a given transition system. The complete proof strategy reduces partial correctness to invariance. For the latter we propose an incremental verification technique for dealing with the case-explosion problem that is known to affect it. All these combined techniques were instrumental in enabling us to prove, within reasonable time and effort limits, that the nontrivial algorithm implemented in a simple hypervisor that we designed in earlier work meets its expected functional requirements. Available at https://hal.archives-ouvertes.fr/hal-01962912." links: "url": "https://hal.inria.fr/hal-01962912" researchr: "https://researchr.org/publication/rusu%3Ahal-01962912" cites: 0 citedby: 0 journal: "SCP" volume: "186" kind: "article" key: "rusu:hal-01962912" - title: "Extracting a Data Flow Analyser in Constructive Logic" author: - name: "David Cachera" link: "https://researchr.org/alias/david-cachera" - name: "Thomas P. Jensen" link: "https://researchr.org/alias/thomas-p.-jensen" - name: "David Pichardie" link: "https://researchr.org/alias/david-pichardie" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2004" doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2986&spage=385" abstract: "We show how to formalise a constraint-based data flow analysis in the specification language of the Coq proof assistant. This involves defining a dependent type of lattices together with a library of lattice functors for modular construction of complex abstract domains. Constraints are expressed in an intermediate representation that allows for both efficient constraint resolution and correctness proof of the analysis with respect to an operational semantics. The proof of existence of a correct, minimal solution to the constraints is constructive which means that the extraction mechanism of Coq provides a provably correct data flow analyser in ocaml. The library of lattices together with the intermediate representation of constraints are defined in an analysis-independent fashion that provides a basis for a generic framework for proving and extracting static analysers in Coq. Available at http://hal.inria.fr/docs/00/56/46/33/PDF/extractDataFlow-ESOP-nospringerlogo.pdf" links: doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2986&spage=385" tags: - "semantics" - "rule-based" - "intermediate representation" - "data-flow language" - "proof assistant" - "domain analysis" - "analysis" - "static analysis" - "constraints" - "data-flow" - "operational semantics" - "logic" - "data-flow analysis" - "domain-specific language" researchr: "https://researchr.org/publication/CacheraJPR04" cites: 0 citedby: 0 pages: "385-400" booktitle: "ESOP" kind: "inproceedings" key: "CacheraJPR04" - title: "On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Eli Singerman" link: "https://researchr.org/alias/eli-singerman" year: "1999" doi: "http://link.springer.de/link/service/series/0558/bibs/1579/15790178.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/1579/15790178.htm" tags: - "analysis" - "static analysis" - "abstraction" researchr: "https://researchr.org/publication/RusuS99" cites: 0 citedby: 0 pages: "178-192" booktitle: "TACAS" kind: "inproceedings" key: "RusuS99" - title: "Analysis of Slope-Parametric Hybrid Automata" author: - name: "Frédéric Boniol" link: "https://researchr.org/alias/fr%C3%A9d%C3%A9ric-boniol" - name: "Augusto Burgueño" link: "https://researchr.org/alias/augusto-burgue%C3%B1o" - name: "Olivier Roux" link: "https://researchr.org/alias/olivier-roux" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "1997" tags: - "analysis" researchr: "https://researchr.org/publication/BoniolBRR97" cites: 0 citedby: 0 pages: "75-80" booktitle: "hybrid" kind: "inproceedings" key: "BoniolBRR97" - title: "Uniformity for the Decidability of Hybrid Automata" author: - name: "Olivier Roux" link: "https://researchr.org/alias/olivier-roux" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "1996" researchr: "https://researchr.org/publication/RouxR96" cites: 0 citedby: 0 pages: "301-316" booktitle: "SAS" kind: "inproceedings" key: "RouxR96" - title: "Program equivalence by circular reasoning" author: - name: "Dorel Lucanu" link: "https://researchr.org/alias/dorel-lucanu" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2015" doi: "http://dx.doi.org/10.1007/s00165-014-0319-6" abstract: "We propose a logic and a deductive system for stating and automatically proving the equivalence of programs in deterministic languages having a rewriting-based operational semantics. The deductive system is circular in nature and is proved sound and weakly complete; together, these results say that, when it terminates, our system correctly solves the program-equivalence problem as we state it. We show that our approach is suitable for proving the equivalence of both terminating and non-terminating programs, and also the equivalence of both concrete and symbolic programs. The latter are programs in which some statements or expressions are symbolic variables. By proving the equivalence between symbolic programs, one proves in one shot the equivalence of (possibly, infinitely) many concrete programs obtained by replacing the variables by concrete statements or expressions. A prototype of the proof system for a particular language was implemented and can be tested on-line. PDF available at https://hal.inria.fr/hal-01076641." links: doi: "http://dx.doi.org/10.1007/s00165-014-0319-6" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/fac/LucanuR15" researchr: "https://researchr.org/publication/LucanuR15" cites: 0 citedby: 0 journal: "fac" volume: "27" number: "4" pages: "701-726" kind: "article" key: "LucanuR15" - title: "Combining formal verification and conformance testing for validating reactive systems" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2003" doi: "http://dx.doi.org/10.1002/stvr.274" links: doi: "http://dx.doi.org/10.1002/stvr.274" tags: - "testing" researchr: "https://researchr.org/publication/Rusu03%3A0" cites: 0 citedby: 0 journal: "stvr" volume: "13" number: "3" pages: "157-180" kind: "article" key: "Rusu03:0" - title: "STG: A Symbolic Test Generation Tool" author: - name: "Duncan Clarke" link: "https://researchr.org/alias/duncan-clarke" - name: "Thierry Jéron" link: "https://researchr.org/alias/thierry-j%C3%A9ron" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Elena Zinovieva" link: "https://researchr.org/alias/elena-zinovieva" year: "2002" doi: "http://link.springer.de/link/service/series/0558/bibs/2280/22800470.htm" abstract: "Applying formal methods to testing has recently become a quite popular research topic. In this paper we explore the opposite approach, namely, applying testing techniques to formal verification. The idea is to use test generation techniques to extract subsets (called components) from a specification and to perform the verification on the components rather than on the whole system. This may considerably reduce the verification effort and, under reasonable sufficient conditions, a safety property verified on a component also holds on the whole specification." links: doi: "http://link.springer.de/link/service/series/0558/bibs/2280/22800470.htm" tags: - "testing" - "systematic-approach" researchr: "https://researchr.org/publication/ClarkeJRZ02" cites: 0 citedby: 0 pages: "470-475" booktitle: "TACAS" kind: "inproceedings" key: "ClarkeJRZ02" - title: "A K-Based Formal Framework for Domain-Specific Modelling Languages" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Dorel Lucanu" link: "https://researchr.org/alias/dorel-lucanu" year: "2011" abstract: "We propose a formal approach for the definition of domain-specific modelling languages (DSMLs). The approach uses basic Model-Driven Engineering artifacts for defining a DSML's syntax (using metamodels) and its operational semantics (using model transformations). We give formal meanings to these artifacts by mapping them to the K semantic framework. The mapping is implemented in the Rascal metaprogramming language. Since the resulting K definitions are executable, one obtains an execution engine for DSMLs and gains acces to K's formal analysis tools. We illustrate the approach on xSPEM, a language for describing the execution of tasks constrained by time, precedence, and resources." researchr: "https://researchr.org/publication/preprint-RusuL11" cites: 0 citedby: 0 type: "Preprint" kind: "techreport" key: "preprint-RusuL11" - title: "Proving Reachability-Logic Formulas Incrementally" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Andrei Arusoaie" link: "https://researchr.org/alias/andrei-arusoaie" year: "2016" abstract: "Reachability Logic (RL) is a formalism for defining the operational semantics of programming languages and for specifying program properties. As a program logic it can be seen as a language-independent alternative to Hoare Logics. Several verification techniques have been proposed for RL, all of which have a circular nature: the RL formula under proof can circularly be used as a hypothesis in the proof of another RL formula, or even in its own proof. This feature is essential for dealing with possibly unbounded repetitive behaviour (e.g., program loops). The downside of such approaches is that the verification of a set of RL formulas is monolithic, i.e., either all formulas in the set are proved valid, or nothing can be inferred about any of the formula's validity or invalidity. In this paper we propose a new, incremental method for proving a large class of RL formulas. The proposed method takes as input a given RL formula under proof (corresponding to a given program fragment), together with a (possibly empty) set of other valid RL formulas (e.g., already proved using our method), which specify sub-programs of the program fragment under verification. It then checks certain conditions are shown to be equivalent to the validity of the RL formula under proof. A newly proved formula can then be incrementally used in the proof of other RL formulas, corresponding to larger program fragments. The process is repeated until the whole program is proved. We illustrate our approach by verifying the nontrivial Knuth-Morris-Pratt string-matching program. PDF available at https://hal.inria.fr/hal-01282379." researchr: "https://researchr.org/publication/RusuArusoaie2016" cites: 0 citedby: 0 booktitle: "Proc. 11th International Workshop on Rewriting Logic and its Applications" kind: "inproceedings" key: "RusuArusoaie2016" - title: "Verifying Periodic Task-Control Systems" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "1997" tags: - "control systems" researchr: "https://researchr.org/publication/Rusu97" cites: 0 citedby: 0 pages: "63-68" booktitle: "hybrid" kind: "inproceedings" key: "Rusu97" - title: "Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Hervé Marchand" link: "https://researchr.org/alias/herv%C3%A9-marchand" - name: "Thierry Jéron" link: "https://researchr.org/alias/thierry-j%C3%A9ron" year: "2005" doi: "http://dx.doi.org/10.1007/11526841_14" abstract: "This paper presents a combination of verification and conformance testing techniques for the formal validation of reactive systems. A formal specification of a system, which may be infinite-state, and a set of safety properties are assumed. Each property is verified on the specification using automatic techniques based on abstract interpretation, which are sound, but, as a price to pay for automation, are not necessarily complete. Next, for each property, a test case is automatically generated from the specification and the property, and is executed on a black-box implementation of the system to detect violations of the property by the implementation and non-conformances between implementation and specification. If the verification step did not conclude, the test execution may also detect violations of the property by the specification. Available at http://hal.inria.fr/docs/00/56/46/25/PDF/fm05.pdf" links: doi: "http://dx.doi.org/10.1007/11526841_14" tags: - "rule-based" - "completeness" - "testing" researchr: "https://researchr.org/publication/RusuMJ05" cites: 0 citedby: 0 pages: "189-204" booktitle: "FM" kind: "inproceedings" key: "RusuMJ05" - title: "(Co)inductive Proof Systems for Compositional Proofs in Reachability Logic" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "David Nowak" link: "https://researchr.org/alias/david-nowak" year: "2020" abstract: "Reachability Logic is a formalism that can be used, among others, for expressing partial-correctness properties of transition systems. In this paper we present three proof systems for this formalism, all of which are sound and complete and inherit the coinductive nature of the logic. The proof systems differ, however, in several aspects. First, they use induction and coinduction in different proportions. The second aspect regards compositionality, broadly meaning their ability to prove simpler formulas on smaller systems and to reuse those formulas as lemmas for proving more complex formulas on larger systems. The third aspect is the difficulty of their soundness proofs. We show that the more induction a proof system uses, and the more specialised is its use of coinduction (with respect to our problem domain), the more compositional the proof system is, but the more difficult is its soundness proof. We present formalisations of these results in the Coq proof assistant. In particular we have developed support for coinductive proofs that is comparable to that provided by Coq for inductive proofs. This may be of interest to a broader class of Coq users." links: published: "https://researchr.org/publication/rn20" researchr: "https://researchr.org/publication/preprint-rn20" cites: 0 citedby: 0 type: "Preprint" kind: "techreport" key: "preprint-rn20" - title: "A Generic Tool for Tracing Executions Back to a DSML s Operational Semantics" author: - name: "Benoît Combemale" link: "https://researchr.org/alias/beno%C3%AEt-combemale" - name: "Laure Gonnord" link: "https://researchr.org/alias/laure-gonnord" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2011" doi: "http://dx.doi.org/10.1007/978-3-642-21470-7_4" abstract: "The increasing complexity of software development requires rigorously defined domain specific modeling languages (DSML). Model-driven engineering (\\mde) allows users to define a DSML's syntax in terms of metamodels. The behaviour of a language can also be described, either operationally, or via transformations to other languages (e.g., by code generation). If the first approach requires to redefine analysis tools for each DSML (simulator, model-checker...), the second approach allows to reuse existing tools in the targeted language. However, the second approach (also called translational semantics) imply that the results (e.g., a program crash log, or a counterexample returned by a model checker) may not be straightforward to interpret by the users of a DSML. We propose in this paper a generic tool for formally tracing such analysis/execution results back to the original DSML's syntax and operational semantics, and we illustrate it on xSPEM, a timed process modeling language. Available at http://hal.archives-ouvertes.fr/hal-00593425." links: doi: "http://dx.doi.org/10.1007/978-3-642-21470-7_4" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ecmdafa/CombemaleGR11" tags: - "semantics" - "operational semantics" researchr: "https://researchr.org/publication/CombemaleGR11" cites: 0 citedby: 0 pages: "35-51" booktitle: "ECMDA-FA" kind: "inproceedings" key: "CombemaleGR11" - title: "Automated Test and Oracle Generation for Smart-Card Applications" author: - name: "Duncan Clarke" link: "https://researchr.org/alias/duncan-clarke" - name: "Thierry Jéron" link: "https://researchr.org/alias/thierry-j%C3%A9ron" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Elena Zinovieva" link: "https://researchr.org/alias/elena-zinovieva" year: "2001" doi: "http://link.springer.de/link/service/series/0558/bibs/2140/21400058.htm" abstract: "We present work we are engaged in to develop symbolic test generation techniques and apply those techniques to testing of smart card applications. Beginning with a system specification and a test purpose expressed as symbolic labelled transition systems we automatically derive tests to check conformance of an implementation to the behaviors of the specification selected by the test purpose. We present an example taken from a case study we are developing based on the application of these techniques to the CEPS e-purse specifications. " links: doi: "http://link.springer.de/link/service/series/0558/bibs/2140/21400058.htm" tags: - "rule-based" - "case study" - "testing" - "e-science" researchr: "https://researchr.org/publication/ClarkeJRZ01" cites: 0 citedby: 0 pages: "58-70" booktitle: "esmart" kind: "inproceedings" key: "ClarkeJRZ01" - title: "Language Definitions as Rewrite Theories" author: - name: "Andrei Arusoaie" link: "https://researchr.org/alias/andrei-arusoaie" - name: "Dorel Lucanu" link: "https://researchr.org/alias/dorel-lucanu" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Traian-Florin Serbanuta" link: "https://researchr.org/alias/traian-florin-serbanuta" - name: "Andrei Stefanescu" link: "https://researchr.org/alias/andrei-stefanescu" - name: "Grigore Rosu" link: "http://fsl.cs.uiuc.edu/~grosu/" year: "2014" doi: "http://dx.doi.org/10.1007/978-3-319-12904-4_5" links: doi: "http://dx.doi.org/10.1007/978-3-319-12904-4_5" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/wrla/ArusoaieLRSSR14" researchr: "https://researchr.org/publication/ArusoaieLRSSR14" cites: 0 citedby: 0 pages: "97-112" booktitle: "WRLA" kind: "inproceedings" key: "ArusoaieLRSSR14" - title: "Verifying Time-bounded Properties for ELECTRE Reactive Programs with Stopwatch Automata" author: - name: "Olivier Roux" link: "https://researchr.org/alias/olivier-roux" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "1994" tags: - "reactive programming" - "program verification" researchr: "https://researchr.org/publication/RouxR94" cites: 0 citedby: 0 pages: "405-416" booktitle: "hybrid" kind: "inproceedings" key: "RouxR94" - title: "Extracting a data flow analyser in constructive logic" author: - name: "David Cachera" link: "https://researchr.org/alias/david-cachera" - name: "Thomas P. Jensen" link: "https://researchr.org/alias/thomas-p.-jensen" - name: "David Pichardie" link: "https://researchr.org/alias/david-pichardie" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2005" doi: "http://dx.doi.org/10.1016/j.tcs.2005.06.004" abstract: "A constraint-based data flow analysis is formalised in the specification language of the Coq proof assistant. This involves defining a dependent type of lattices together with a library of lattice functors for modular construction of complex abstract domains. Constraints are represented in a way that allows for both efficient constraint resolution and correctness proof of the analysis with respect to an operational semantics. The proof of existence of a solution to the constraints is constructive which means that the extraction mechanism of Coq provides a provably correct data flow analyser in Ocaml from the proof. The library of lattices and the representation of constraints are defined in an analysis-independent fashion that provides a basis for a generic framework for proving and extracting static analysers in Coq. Available at http://hal.inria.fr/docs/00/56/46/11/PDF/extract-tcs.pdf" links: doi: "http://dx.doi.org/10.1016/j.tcs.2005.06.004" "techreport": "http://hal.inria.fr/docs/00/56/46/11/PDF/extract-tcs.pdf" tags: - "semantics" - "rule-based" - "data-flow language" - "proof assistant" - "domain analysis" - "analysis" - "static analysis" - "constraints" - "data-flow" - "operational semantics" - "logic" - "data-flow analysis" - "domain-specific language" researchr: "https://researchr.org/publication/CacheraJPR05" cites: 0 citedby: 0 journal: "TCS" volume: "342" number: "1" pages: "56-78" kind: "article" key: "CacheraJPR05" - title: "Proving Partial-Correctness and Invariance Properties of Transition-System Models" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Gilles Grimaud" link: "https://researchr.org/alias/gilles-grimaud" - name: "Michaël Hauspie" link: "https://researchr.org/alias/micha%C3%ABl-hauspie" year: "2018" month: "Aug" abstract: "We propose a deductive verification approach for proving partial-correctness and invariance properties on transition-system models. Regarding partial correctness, we gen-eralise the recently introduced formalism of Reachability Logic, currently used as a language-parametric logic for programs, to transition systems. We propose a sound and relatively complete proof system for the resulting reachability logic. The soundness of the proof system is formally established in the Coq proof assistant, and the mechanised proof provides us with a Coq-certified Reachability-Logic prover for transition-system models. The relative completeness of the proof system, although theoretical in nature, also has a practical value, as it induces a proof strategy that is guaranteed to prove all valid formulas on a given transition system. The strategy reduces partial-correctness verification to invariance verification; for the latter we propose an incremental technique in order to deal with the case-explosion problem that affects it. All these techniques were instrumental in enabling us to prove, within reasonable time and effort limits, that the nontrivial algorithm implemented in security hypervisor that we designed in earlier work meets its expected functional requirements. PDF available at https://hal.inria.fr/view/index/docid/1895650." links: "url": "https://hal.inria.fr/hal-01816798" researchr: "https://researchr.org/publication/rusu%3Ahal-01816798" cites: 0 citedby: 0 booktitle: "TASE 2018 - 12th International Symposium on Theoretical Aspects of Software Engineering" kind: "inproceedings" key: "rusu:hal-01816798" - title: "An Approach to Symbolic Test Generation" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "Lydie du Bousquet" link: "https://researchr.org/alias/lydie-du-bousquet" - name: "Thierry Jéron" link: "https://researchr.org/alias/thierry-j%C3%A9ron" year: "2000" doi: "http://link.springer.de/link/service/series/0558/bibs/1945/19450338.htm" abstract: "Test generation is a program-synthesis problem: starting from the formal specification of a system under test, and from a test purpose describing a set of behaviours to be tested, compute a reactive program that observes an implementation of the system to detect non-conformant behaviour, while trying to control it towards satisfying the test purpose. In this paper we describe an approach for generating symbolic test cases, in the form of input-output automata with variables and parameters. The pdf file is available in the column located to the left of this abstract." links: doi: "http://link.springer.de/link/service/series/0558/bibs/1945/19450338.htm" technicalreport: "https://researchr.org/publication/preprint-RusuBJ00" tags: - "control systems" - "reactive programming" - "testing" - "programming" - "systematic-approach" researchr: "https://researchr.org/publication/RusuBJ00" cites: 0 citedby: 0 pages: "338-357" booktitle: "IFM" kind: "inproceedings" key: "RusuBJ00" - title: "Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, Thessaloniki, Greece, June 14-15, 2018, Proceedings" year: "2018" doi: "10.1007/978-3-319-99840-4" links: "url": "https://doi.org/10.1007/978-3-319-99840-4" researchr: "https://researchr.org/publication/DBLP%3Aconf-wrla-2018" cites: 0 citedby: 0 booktitle: "Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, Thessaloniki, Greece, June 14-15, 2018, Proceedings" editor: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" volume: "11152" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-319-99839-8" kind: "proceedings" key: "DBLP:conf-wrla-2018" - title: "Proceedings Second International Workshop on Algebraic Methods in Model-based Software Engineering" year: "2011" doi: "10.4204/EPTCS.56" abstract: "Over the past years there has been quite a lot of activity in the algebraic community about using algebraic methods for providing support to model-driven software engineering. The aim of this workshop is to gather researchers working on the development and application of algebraic methods to provide rigorous support to model-based software engineering. The topics relevant to the workshop are all those related to the use of algebraic methods in software engineering, including but not limited to: formally specifying and verifying model-based software engineering concepts and related ones (MDE, UML, OCL, MOF, DSLs, ...); tool support for the above; integration of formal and informal methods; and theoretical frameworks (algebraic, rewriting-based, category theory-based, ...). The workshop's main goal is to examine, discuss, and relate the existing projects within the algebraic community that address common open-issues in model-driven software engineering. " tags: - "OCL" - "rule-based" - "application framework" - "meta-model" - "UML" - "model-driven development" - "source-to-source" - "graph-rewriting" - "software engineering" - "model-driven engineering" - " algebra" - "DSL" - "Meta-Environment" - "rewriting" - "MDE" - "open-source" researchr: "https://researchr.org/publication/DBLP%3Ajournals-corr-abs-1106-5962" cites: 0 citedby: 0 booktitle: "Proceedings Second International Workshop on Algebraic Methods in Model-based Software Engineering" editor: - name: "Francisco Duràn" link: "https://researchr.org/alias/francisco-dur%C3%A0n" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" volume: "56" series: "Electronic Proceedings in Theoretical Computer Science" kind: "proceedings" key: "DBLP:journals-corr-abs-1106-5962"