@inproceedings{VanhemsRNG22, title = {A Formal Correctness Proof for an EDF Scheduler Implementation}, author = {Florian Vanhems and Vlad Rusu and David Nowak and Gilles Grimaud}, year = {2022}, doi = {10.1109/RTAS54340.2022.00030}, url = {https://doi.org/10.1109/RTAS54340.2022.00030}, researchr = {https://researchr.org/publication/VanhemsRNG22}, cites = {0}, citedby = {0}, pages = {281-292}, booktitle = {28th IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2022, Milano, Italy, May 4-6, 2022}, publisher = {IEEE}, isbn = {978-1-6654-9998-9}, } @inproceedings{GamatieRR10, title = {Operational Semantics of the Marte Repetitive Structure Modeling Concepts for Data-Parallel Applications Design}, author = {Abdoulaye Gamatié and Vlad Rusu and Éric Rutten}, year = {2010}, doi = {10.1109/ISPDC.2010.30}, url = {http://doi.ieeecomputersociety.org/10.1109/ISPDC.2010.30}, 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 = {Ninth International Symposium on Parallel and Distributed Computing, ISPDC 2010, Istanbul, Turkey, July 7-9, 2010}, publisher = {IEEE Computer Society}, isbn = {978-0-7695-4120-4}, } @article{Rusu:2011:EDM:1921532.1921557, title = {Embedding domain-specific modelling languages in maude specifications}, author = {Vlad Rusu}, year = {2011}, month = {January}, doi = {10.1145/1921532.1921557}, url = {http://doi.acm.org/10.1145/1921532.1921557}, note = {The PDF link points to the revised version, accepted for publication with minor revisions in the Software and Systems modelling journal}, 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}, } @techreport{preprint-RusuBJ00, title = {An Approach to Symbolic Test Generation}, author = {Vlad Rusu and Lydie du Bousquet and Thierry Jéron}, year = {2000}, researchr = {https://researchr.org/publication/preprint-RusuBJ00}, cites = {0}, citedby = {0}, type = {Preprint}, } @techreport{preprint-Rusu02, title = {Verification Using Test Generation Techniques}, author = {Vlad Rusu}, year = {2002}, researchr = {https://researchr.org/publication/preprint-Rusu02}, cites = {0}, citedby = {0}, type = {Preprint}, } @inproceedings{Rusu02, title = {Verification Using Test Generation Techniques}, author = {Vlad Rusu}, year = {2002}, url = {http://link.springer.de/link/service/series/0558/bibs/2391/23910252.htm}, tags = {testing}, researchr = {https://researchr.org/publication/Rusu02}, cites = {0}, citedby = {0}, pages = {252-271}, booktitle = {FME 2002: Formal Methods - Getting IT Right, International Symposium of Formal Methods Europe, Copenhagen, Denmark, July 22-24, 2002, Proceedings}, editor = {Lars-Henrik Eriksson and Peter A. Lindsay}, volume = {2391}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {3-540-43928-5}, } @article{RusuZ01, title = {Analyzing Automata with Presburger Arithmetic and Uninterpreted Function Symbols}, author = {Vlad Rusu and Elena Zinovieva}, year = {2001}, url = {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 = {Electronic Notes in Theoretical Computer Science}, volume = {50}, number = {4}, pages = {327-341}, } @inproceedings{RusuMTJJ04, title = {From Safety Verification to Safety Testing}, author = {Vlad Rusu and Hervé Marchand and Valéry Tschaen and Thierry Jéron and Bertrand Jeannet}, year = {2004}, url = {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}, } @article{Rusu13, title = {Embedding domain-specific modelling languages in Maude specifications}, author = {Vlad Rusu}, year = {2013}, doi = {10.1007/s10270-012-0232-5}, url = {http://dx.doi.org/10.1007/s10270-012-0232-5}, researchr = {https://researchr.org/publication/Rusu13}, cites = {0}, citedby = {0}, journal = {Software and Systems Modeling}, volume = {12}, number = {4}, pages = {847-869}, } @article{GenetR10, title = {Equational approximations for tree automata completion}, author = {Thomas Genet and Vlad Rusu}, year = {2010}, doi = {10.1016/j.jsc.2010.01.009}, url = {http://dx.doi.org/10.1016/j.jsc.2010.01.009}, tags = {meta-model, term rewriting, graph-rewriting, e-science, Meta-Environment, rewriting}, researchr = {https://researchr.org/publication/GenetR10}, cites = {0}, citedby = {0}, journal = {Journal of Symbolic Computation}, volume = {45}, number = {5}, pages = {574-597}, } @inproceedings{ClarkeJRZ01:0, title = {STG: a tool for generating symbolic test programs and oracles from operational specifications}, author = {Duncan Clarke and Thierry Jéron and Vlad Rusu and Elena Zinovieva}, year = {2001}, doi = {10.1145/503209.503252}, url = {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 / SIGSOFT FSE}, } @inproceedings{JeannetJRZ05, title = {Symbolic Test Selection Based on Approximate Analysis}, author = {Bertrand Jeannet and Thierry Jéron and Vlad Rusu and Elena Zinovieva}, year = {2005}, url = {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 = {Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings}, editor = {Nicolas Halbwachs and Lenore D. Zuck}, volume = {3440}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {3-540-25333-5}, } @article{ConstantJMR07, title = {Integrating formal verification and conformance testing for reactive systems}, author = {Camille Constant and Thierry Jéron and Hervé Marchand and Vlad Rusu}, year = {2007}, doi = {10.1109/TSE.2007.70707}, url = {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 = {IEEE Trans. Software Eng.}, volume = {33}, number = {8}, pages = {558-574}, } @article{EgeaR10, title = {Formal executable semantics for conformance in the MDE framework}, author = {Marina Egea and Vlad Rusu}, year = {2010}, doi = {10.1007/s11334-009-0108-1}, url = {http://dx.doi.org/10.1007/s11334-009-0108-1}, 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}, } @techreport{preprint-Rusu03, title = {Compositional Verification of an ATM Protocol}, author = {Vlad Rusu}, year = {2003}, researchr = {https://researchr.org/publication/preprint-Rusu03}, cites = {0}, citedby = {0}, type = {Preprint}, } @techreport{preprint-RouxRC99, title = {Hybrid Verifications of Reactive Programs}, author = {Olivier Roux and Vlad Rusu and Franck Cassez}, year = {1999}, researchr = {https://researchr.org/publication/preprint-RouxRC99}, cites = {0}, citedby = {0}, type = {Preprint}, } @techreport{preprint-rusu:hal-01186005, title = {Language Definitions as Rewrite Theories}, author = {Vlad Rusu and Lucanu, Dorel and Serbanuta, Traian Florin and Arusoaie, Andrei and Stefanescu, Andrei and Grigore Rosu}, year = {2015}, researchr = {https://researchr.org/publication/preprint-rusu%3Ahal-01186005}, cites = {0}, citedby = {0}, type = {Preprint}, } @article{rusu:inria-00564219, title = {Vérification d'invariants pour des systèmes spécifiés en logique de réécriture}, author = {Vlad Rusu and Clavel, Manuel}, year = {2009}, 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}, } @article{rn20, title = {(Co)inductive Proof Systems for Compositional Proofs in Reachability Logic}, author = {Vlad Rusu and David Nowak}, year = {2021}, month = {January}, doi = {10.1016/j.jlamp.2020.100619}, url = {https://doi.org/10.1016/j.jlamp.2020.100619}, researchr = {https://researchr.org/publication/rn20}, cites = {0}, citedby = {0}, journal = {J. Log. Algebr. Meth. Program.}, volume = {118}, } @inproceedings{JeannetJR06, title = {Model-Based Test Selection for Infinite-State Reactive Systems}, author = {Bertrand Jeannet and Thierry Jéron and Vlad Rusu}, year = {2006}, doi = {10.1007/978-3-540-74792-5_3}, url = {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 = {Formal Methods for Components and Objects, 5th International Symposium, FMCO 2006, Amsterdam, The Netherlands, November 7-10, 2006, Revised Lectures}, editor = {Frank S. de Boer and Marcello M. Bonsangue and Susanne Graf and Willem P. de Roever}, volume = {4709}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-540-74791-8}, } @article{Rusu21, title = {Guest Editor's foreword}, author = {Vlad Rusu}, year = {2021}, doi = {10.1016/j.jlamp.2021.100716}, url = {https://doi.org/10.1016/j.jlamp.2021.100716}, researchr = {https://researchr.org/publication/Rusu21}, cites = {0}, citedby = {0}, journal = {J. Log. Algebr. Meth. Program.}, volume = {123}, pages = {100716}, } @inproceedings{Rusu01, title = {Verifying a Sliding Window Protocol using PVS}, author = {Vlad Rusu}, year = {2001}, 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 = {Formal Techniques for Networked and Distributed Systems, FORTE 2001, IFIP TC6/WG6.1 - 21:::st::: International Conference on Formal Techniques for Networked and Distributed Systems, August 28-31, 2001, Cheju Island, Korea}, editor = {Myungchul Kim and Byoungmoon Chin and Sungwon Kang and Danhyung Lee}, volume = {197}, series = {IFIP Conference Proceedings}, publisher = {Kluwer}, isbn = {0-7923-7470-3}, } @inproceedings{OostdijkRTVW07, title = {Integrating Verification, Testing, and Learning for Cryptographic Protocols}, author = {Martijn Oostdijk and Vlad Rusu and Jan Tretmans and René G. de Vries and Tim A. C. Willemse}, year = {2007}, doi = {10.1007/978-3-540-73210-5_28}, url = {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 = {Integrated Formal Methods, 6th International Conference, IFM 2007, Oxford, UK, July 2-5, 2007, Proceedings}, editor = {Jim Davies and Jeremy Gibbons}, volume = {4591}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-540-73209-9}, } @techreport{preprint-ArusoaieLucanuNowakand-Vlad-Rusu2015-0, title = {Verifying Reachability-Logic Properties on Rewriting-Logic Specifications}, author = {Andrei Arusoaie and Dorel Lucanu and David Nowak and Vlad Rusu}, year = {2015}, researchr = {https://researchr.org/publication/preprint-ArusoaieLucanuNowakand-Vlad-Rusu2015-0}, cites = {0}, citedby = {0}, type = {Preprint}, } @inproceedings{Rusu03, title = {Compositional Verification of an ATM Protocol}, author = {Vlad Rusu}, year = {2003}, url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2805&spage=223}, tags = {rule-based, protocol, composition, data-flow, abstraction, systematic-approach}, researchr = {https://researchr.org/publication/Rusu03}, cites = {0}, citedby = {0}, pages = {223-243}, booktitle = {FME 2003: Formal Methods, International Symposium of Formal Methods Europe, Pisa, Italy, September 8-14, 2003, Proceedings}, editor = {Keijiro Araki and Stefania Gnesi and Dino Mandrioli}, volume = {2805}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {3-540-40828-2}, } @article{jeron04a, title = {Ensuring the conformance of reactive discrete-event systems by means of supervisory control}, author = {Jeron, T. and Marchand, H. and Vlad Rusu and Tschaen, V.}, year = {2004}, tags = {control systems, testing}, researchr = {https://researchr.org/publication/jeron04a}, cites = {0}, citedby = {0}, journal = {International Journal of Production Research}, volume = {42}, number = {14}, } @article{ArusoaieLR14, title = {Towards a K Semantics for OCL}, author = {Andrei Arusoaie and Dorel Lucanu and Vlad Rusu}, year = {2014}, doi = {10.1016/j.entcs.2014.05.004}, url = {http://dx.doi.org/10.1016/j.entcs.2014.05.004}, researchr = {https://researchr.org/publication/ArusoaieLR14}, cites = {0}, citedby = {0}, journal = {Electronic Notes in Theoretical Computer Science}, volume = {304}, pages = {81-96}, } @article{CiobacaLRR16, title = {A language-independent proof system for full program equivalence}, author = {Stefan Ciobaca and Dorel Lucanu and Vlad Rusu and Grigore Rosu}, year = {2016}, doi = {10.1007/s00165-016-0361-7}, url = {http://dx.doi.org/10.1007/s00165-016-0361-7}, researchr = {https://researchr.org/publication/CiobacaLRR16}, cites = {0}, citedby = {0}, journal = {Formal Asp. Comput.}, volume = {28}, number = {3}, pages = {469-497}, } @article{RusuA17-0, title = {Executing and verifying higher-order functional-imperative programs in Maude}, author = {Vlad Rusu and Andrei Arusoaie}, year = {2017}, doi = {10.1016/j.jlamp.2017.09.002}, url = {https://doi.org/10.1016/j.jlamp.2017.09.002}, researchr = {https://researchr.org/publication/RusuA17-0}, cites = {0}, citedby = {0}, journal = {Journal of Logic and Algebraic Programming}, volume = {93}, pages = {68-91}, } @article{LucanuRA17, title = {A generic framework for symbolic execution: A coinductive approach}, author = {Dorel Lucanu and Vlad Rusu and Andrei Arusoaie}, year = {2017}, doi = {10.1016/j.jsc.2016.07.012}, url = {http://dx.doi.org/10.1016/j.jsc.2016.07.012}, researchr = {https://researchr.org/publication/LucanuRA17}, cites = {0}, citedby = {0}, journal = {Journal of Symbolic Computation}, volume = {80}, pages = {125-163}, } @inproceedings{Rusu10, title = {Combining Theorem Proving and Narrowing for Rewriting-Logic Specifications}, author = {Vlad Rusu}, year = {2010}, doi = {10.1007/978-3-642-13977-2_12}, url = {http://dx.doi.org/10.1007/978-3-642-13977-2_12}, 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 = {Tests and Proofs, 4th International Conference, TAP 2010, Málaga, Spain, July 1-2, 2010. Proceedings}, editor = {Gordon Fraser and Angelo Gargantini}, volume = {6143}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-642-13976-5}, } @inproceedings{BurguenoR97, title = {Task-System Analysis Using Slope-Parametric Hybrid Automata}, author = {Augusto Burgueño and Vlad Rusu}, year = {1997}, tags = {analysis}, researchr = {https://researchr.org/publication/BurguenoR97}, cites = {0}, citedby = {0}, pages = {1262-1273}, booktitle = {Euro-Par 97 Parallel Processing, Third International Euro-Par Conference, Passau, Germany, August 26-29, 1997, Proceedings}, editor = {Christian Lengauer and Martin Griebl and Sergei Gorlatch}, volume = {1300}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {3-540-63440-1}, } @article{Rusu06, title = {Verifying an ATM Protocol Using a Combination of Formal Techniques}, author = {Vlad Rusu}, year = {2006}, doi = {10.1093/comjnl/bxl039}, url = {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 = {Comput. J.}, volume = {49}, number = {6}, pages = {710-730}, } @inproceedings{JeronMR06, title = {Symbolic Determinisation of Extended Automata}, author = {Thierry Jéron and Hervé Marchand and Vlad Rusu}, year = {2006}, doi = {10.1007/978-0-387-34735-6_18}, url = {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 = {Fourth IFIP International Conference on Theoretical Computer Science (TCS 2006), IFIP 19th World Computer Congress, TC-1 Foundations of Computer Science, August 23-24, 2006, Santiago, Chile}, editor = {Gonzalo Navarro and Leopoldo E. Bertossi and Yoshiharu Kohayakawa}, volume = {209}, series = {IFIP}, publisher = {Springer}, isbn = {0-387-34633-3}, } @inproceedings{BartheFPR06, title = {Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant}, author = {Gilles Barthe and Julien Forest and David Pichardie and Vlad Rusu}, year = {2006}, doi = {10.1007/11737414_9}, url = {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 = {Functional and Logic Programming, 8th International Symposium, FLOPS 2006, Fuji-Susono, Japan, April 24-26, 2006, Proceedings}, editor = {Masami Hagiya and Philip Wadler}, volume = {3945}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {3-540-33438-6}, } @inproceedings{CiobacaLRR14-0, title = {A Theoretical Foundation for Programming Languages Aggregation}, author = {Stefan Ciobaca and Dorel Lucanu and Vlad Rusu and Grigore Rosu}, year = {2014}, doi = {10.1007/978-3-319-28114-8_3}, url = {http://dx.doi.org/10.1007/978-3-319-28114-8_3}, researchr = {https://researchr.org/publication/CiobacaLRR14-0}, cites = {0}, citedby = {0}, pages = {30-47}, booktitle = {Recent Trends in Algebraic Development Techniques - 22nd International Workshop, WADT 2014, Sinaia, Romania, September 4-7, 2014, Revised Selected Papers}, editor = {Mihai Codescu and Razvan Diaconescu and Ionut Tutu}, volume = {9463}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-319-28113-1}, } @incollection{book-chap-react-systems, title = {Validation of Reactive Systems}, author = {Constant, C. and Jeron, T. and Marchand, H. and Vlad Rusu}, 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}, } @inproceedings{ArusoaieLucanuNowakand-Vlad-Rusu2015-0, title = {Verifying Reachability-Logic Properties on Rewriting-Logic Specifications}, author = {Dorel Lucanu and Vlad Rusu and Andrei Arusoaie and David Nowak}, year = {2015}, note = {To appear in LNCS}, 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}, series = {LNCS}, } @article{RouxRC99, title = {Hybrid Verifications of Reactive Programs}, author = {Olivier Roux and Vlad Rusu and Franck Cassez}, year = {1999}, url = {http://link.springer.de/link/service/journals/00165/bibs/9011004/90110448.htm}, tags = {reactive programming, program verification, programming}, researchr = {https://researchr.org/publication/RouxRC99}, cites = {0}, citedby = {0}, journal = {Formal Asp. Comput.}, volume = {11}, number = {4}, pages = {448-471}, } @techreport{preprint-lucanu:hal-01065830, title = {Program Equivalence by Circular Reasoning}, author = {Lucanu, Dorel and Vlad Rusu}, year = {2014}, researchr = {https://researchr.org/publication/preprint-lucanu%3Ahal-01065830}, cites = {0}, citedby = {0}, type = {Preprint}, } @inproceedings{CiobacaLRR14, title = {A Language-Independent Proof System for Mutual Program Equivalence}, author = {Stefan Ciobaca and Dorel Lucanu and Vlad Rusu and Grigore Rosu}, year = {2014}, doi = {10.1007/978-3-319-11737-9_6}, url = {http://dx.doi.org/10.1007/978-3-319-11737-9_6}, researchr = {https://researchr.org/publication/CiobacaLRR14}, cites = {0}, citedby = {0}, pages = {75-90}, booktitle = {Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, ICFEM 2014, Luxembourg, Luxembourg, November 3-5, 2014. Proceedings}, editor = {Stephan Merz and Jun Pang}, volume = {8829}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-319-11736-2}, } @inproceedings{ArusoaieLR13, title = {A Generic Framework for Symbolic Execution}, author = {Andrei Arusoaie and Dorel Lucanu and Vlad Rusu}, year = {2013}, doi = {10.1007/978-3-319-02654-1_16}, url = {http://dx.doi.org/10.1007/978-3-319-02654-1_16}, researchr = {https://researchr.org/publication/ArusoaieLR13}, cites = {0}, citedby = {0}, pages = {281-301}, booktitle = {Software Language Engineering - 6th International Conference, SLE 2013, Indianapolis, IN, USA, October 26-28, 2013. Proceedings}, editor = {Martin Erwig and Richard F. Paige and Eric {Van Wyk}}, volume = {8225}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-319-02653-4}, } @inproceedings{RusuN22-0, title = {Defining Corecursive Functions in Coq Using Approximations}, author = {Vlad Rusu and David Nowak}, year = {2022}, doi = {10.4230/LIPIcs.ECOOP.2022.12}, url = {https://doi.org/10.4230/LIPIcs.ECOOP.2022.12}, researchr = {https://researchr.org/publication/RusuN22-0}, cites = {0}, citedby = {0}, booktitle = {36th European Conference on Object-Oriented Programming, ECOOP 2022, June 6-10, 2022, Berlin, Germany}, editor = {Karim Ali 0001 and Jan Vitek}, volume = {222}, series = {LIPIcs}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, isbn = {978-3-95977-225-9}, } @inproceedings{ciobaca:hal-01076641, title = {A theoretical foundation for programming languages aggregation}, author = {Stefan Ciobaca and Dorel Lucanu and Vlad Rusu and Grigore Rosu}, year = {2015}, 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}, volume = {9463}, series = {LNCS}, address = {Sinaia, Romania}, publisher = {Spriger Verlag}, } @inproceedings{RusuL11, title = {A K-Based Formal Framework for Domain-Specific Modelling Languages}, author = {Vlad Rusu and Dorel Lucanu}, year = {2011}, doi = {10.1007/978-3-642-31762-0_14}, url = {http://dx.doi.org/10.1007/978-3-642-31762-0_14}, researchr = {https://researchr.org/publication/RusuL11}, cites = {0}, citedby = {0}, pages = {214-231}, booktitle = {Formal Verification of Object-Oriented Software - International Conference, FoVeOOS 2011, Turin, Italy, October 5-7, 2011, Revised Selected Papers}, editor = {Bernhard Beckert and Ferruccio Damiani and Dilian Gurov}, volume = {7421}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-642-31761-3}, } @article{rusu:hal-01186005, title = {Language Definitions as Rewrite Theories}, author = {Vlad Rusu and Dorel Lucanu and Traian-Florin Serbanuta and Andrei Arusoaie and Andrei Stefanescu and Grigore Rosu}, year = {2016}, month = {January}, url = {https://hal.inria.fr/hal-01186005}, note = {To appear.}, researchr = {https://researchr.org/publication/rusu%3Ahal-01186005}, cites = {0}, citedby = {0}, journal = {Journal of Logic and Algebraic Methods in Programming}, volume = {85}, number = {1 Part 1}, pages = {98-120}, } @inproceedings{DBLP:journals-corr-abs-1909-01744, title = {(Co)inductive Proof Systems for Compositional Proofs in Reachability Logic}, author = {Vlad Rusu and David Nowak}, year = {2019}, doi = {10.4204/EPTCS.303.3}, 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}, } @inproceedings{HenzingerR98, title = {Reachability Verification for Hybrid Automata}, author = {Thomas A. Henzinger and Vlad Rusu}, year = {1998}, researchr = {https://researchr.org/publication/HenzingerR98}, cites = {0}, citedby = {0}, pages = {190-204}, booktitle = {Hybrid Systems: Computation and Control, First International Workshop, HSCC 98, Berkeley, California, USA, April 13-15, 1998, Proceedings}, editor = {Thomas A. Henzinger and Shankar Sastry}, volume = {1386}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {3-540-64358-3}, } @article{roux94, title = {Translating from GRAFCET to the reactive language ELECTRE}, author = {Roux, O. and Vlad Rusu}, year = {1994}, tags = {translation}, researchr = {https://researchr.org/publication/roux94}, cites = {0}, citedby = {0}, journal = {Automatique, Productique et Informatique Industrielle}, volume = {28}, number = {2}, } @inproceedings{LucanuR13, title = {Program Equivalence by Circular Reasoning}, author = {Dorel Lucanu and Vlad Rusu}, year = {2013}, doi = {10.1007/978-3-642-38613-8_25}, url = {http://dx.doi.org/10.1007/978-3-642-38613-8_25}, researchr = {https://researchr.org/publication/LucanuR13}, cites = {0}, citedby = {0}, pages = {362-377}, booktitle = {Integrated Formal Methods, 10th International Conference, IFM 2013, Turku, Finland, June 10-14, 2013. Proceedings}, editor = {Einar Broch Johnsen and Luigia Petre}, volume = {7940}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-642-38613-8}, } @article{ArusoaieLR15, title = {Symbolic execution based on language transformation}, author = {Andrei Arusoaie and Dorel Lucanu and Vlad Rusu}, year = {2015}, doi = {10.1016/j.cl.2015.08.004}, url = {http://dx.doi.org/10.1016/j.cl.2015.08.004}, researchr = {https://researchr.org/publication/ArusoaieLR15}, cites = {0}, citedby = {0}, journal = {Computer Languages, Systems \& Structures}, volume = {44}, pages = {48-71}, } @article{rusu:hal-01962912, title = {Proving Partial-Correctness and Invariance Properties of Transition-System Models}, author = {Vlad Rusu and Gilles Grimaud and Michaël Hauspie}, year = {2020}, month = {February}, doi = {10.1016/j.scico.2019.102342}, url = {https://hal.inria.fr/hal-01962912}, researchr = {https://researchr.org/publication/rusu%3Ahal-01962912}, cites = {0}, citedby = {0}, journal = {Science of Computer Programming}, volume = {186}, } @inproceedings{CacheraJPR04, title = {Extracting a Data Flow Analyser in Constructive Logic}, author = {David Cachera and Thomas P. Jensen and David Pichardie and Vlad Rusu}, year = {2004}, url = {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 = {Programming Languages and Systems, 13th European Symposium on Programming, ESOP 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings}, editor = {David A. Schmidt}, volume = {2986}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {3-540-21313-9}, } @inproceedings{RusuS99, title = {On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction}, author = {Vlad Rusu and Eli Singerman}, year = {1999}, url = {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 = {Tools and Algorithms for Construction and Analysis of Systems, 5th International Conference, TACAS 99, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 99, Amsterdam, The Netherlands, March 22-28, 1999, Proceed}, editor = {Rance Cleaveland}, volume = {1579}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {3-540-65703-7}, } @inproceedings{BoniolBRR97, title = {Analysis of Slope-Parametric Hybrid Automata}, author = {Frédéric Boniol and Augusto Burgueño and Olivier Roux and Vlad Rusu}, year = {1997}, tags = {analysis}, researchr = {https://researchr.org/publication/BoniolBRR97}, cites = {0}, citedby = {0}, pages = {75-80}, booktitle = {Hybrid and Real-Time Systems, International Workshop. HART 97, Grenoble, France, March 26-28, 1997, Proceedings}, editor = {Oded Maler}, volume = {1201}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {3-540-62600-X}, } @inproceedings{RouxR96, title = {Uniformity for the Decidability of Hybrid Automata}, author = {Olivier Roux and Vlad Rusu}, year = {1996}, researchr = {https://researchr.org/publication/RouxR96}, cites = {0}, citedby = {0}, pages = {301-316}, booktitle = {Static Analysis, Third International Symposium, SAS 96, Aachen, Germany, September 24-26, 1996, Proceedings}, editor = {Radhia Cousot and David A. Schmidt}, volume = {1145}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {3-540-61739-6}, } @article{LucanuR15, title = {Program equivalence by circular reasoning}, author = {Dorel Lucanu and Vlad Rusu}, year = {2015}, doi = {10.1007/s00165-014-0319-6}, url = {http://dx.doi.org/10.1007/s00165-014-0319-6}, researchr = {https://researchr.org/publication/LucanuR15}, cites = {0}, citedby = {0}, journal = {Formal Asp. Comput.}, volume = {27}, number = {4}, pages = {701-726}, } @article{Rusu03:0, title = {Combining formal verification and conformance testing for validating reactive systems}, author = {Vlad Rusu}, year = {2003}, doi = {10.1002/stvr.274}, url = {http://dx.doi.org/10.1002/stvr.274}, tags = {testing}, researchr = {https://researchr.org/publication/Rusu03%3A0}, cites = {0}, citedby = {0}, journal = {Softw. Test., Verif. Reliab.}, volume = {13}, number = {3}, pages = {157-180}, } @inproceedings{-24, title = {While Loops in Coq}, author = {David Nowak and Vlad Rusu}, year = {2023}, doi = {10.4204/EPTCS.389.8}, url = {https://doi.org/10.4204/EPTCS.389.8}, researchr = {https://researchr.org/publication/-24}, cites = {0}, citedby = {0}, pages = {96-109}, booktitle = {Proceedings 7th Symposium on Working Formal Methods, FROM 2023, Bucharest, Romania, 21-22 September 2023}, volume = {389}, series = {EPTCS}, } @inproceedings{ClarkeJRZ02, title = {STG: A Symbolic Test Generation Tool}, author = {Duncan Clarke and Thierry Jéron and Vlad Rusu and Elena Zinovieva}, year = {2002}, url = {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 = {Tools and Algorithms for the Construction and Analysis of Systems, 8th International Conference, TACAS 2002, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings}, editor = {Joost-Pieter Katoen and Perdita Stevens}, volume = {2280}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {3-540-43419-4}, } @techreport{preprint-RusuL11, title = {A K-Based Formal Framework for Domain-Specific Modelling Languages}, author = {Vlad Rusu and Dorel Lucanu}, year = {2011}, researchr = {https://researchr.org/publication/preprint-RusuL11}, cites = {0}, citedby = {0}, type = {Preprint}, } @inproceedings{RusuArusoaie2016, title = {Proving Reachability-Logic Formulas Incrementally}, author = {Vlad Rusu and Andrei Arusoaie}, year = {2016}, researchr = {https://researchr.org/publication/RusuArusoaie2016}, cites = {0}, citedby = {0}, booktitle = {Proc. 11th International Workshop on Rewriting Logic and its Applications}, series = {LNCS (to appear)}, publisher = {Springer Verlag}, } @inproceedings{Rusu97, title = {Verifying Periodic Task-Control Systems}, author = {Vlad Rusu}, year = {1997}, tags = {control systems}, researchr = {https://researchr.org/publication/Rusu97}, cites = {0}, citedby = {0}, pages = {63-68}, booktitle = {Hybrid and Real-Time Systems, International Workshop. HART 97, Grenoble, France, March 26-28, 1997, Proceedings}, editor = {Oded Maler}, volume = {1201}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {3-540-62600-X}, } @inproceedings{RusuMJ05, title = {Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems}, author = {Vlad Rusu and Hervé Marchand and Thierry Jéron}, year = {2005}, doi = {10.1007/11526841_14}, url = {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 2005: Formal Methods, International Symposium of Formal Methods Europe, Newcastle, UK, July 18-22, 2005, Proceedings}, editor = {John Fitzgerald and Ian J. Hayes and Andrzej Tarlecki}, volume = {3582}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {3-540-27882-6}, } @techreport{preprint-rn20, title = {(Co)inductive Proof Systems for Compositional Proofs in Reachability Logic}, author = {Vlad Rusu and David Nowak}, year = {2020}, researchr = {https://researchr.org/publication/preprint-rn20}, cites = {0}, citedby = {0}, type = {Preprint}, } @inproceedings{CombemaleGR11, title = {A Generic Tool for Tracing Executions Back to a DSML s Operational Semantics}, author = {Benoît Combemale and Laure Gonnord and Vlad Rusu}, year = {2011}, doi = {10.1007/978-3-642-21470-7_4}, url = {http://dx.doi.org/10.1007/978-3-642-21470-7_4}, tags = {semantics, operational semantics}, researchr = {https://researchr.org/publication/CombemaleGR11}, cites = {0}, citedby = {0}, pages = {35-51}, booktitle = {Modelling Foundations and Applications - 7th European Conference, ECMFA 2011, Birmingham, UK, June 6 - 9, 2011 Proceedings}, editor = {Robert B. France and Jochen Malte Kuester and Behzad Bordbar and Richard F. Paige}, volume = {6698}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-642-21469-1}, } @inproceedings{ClarkeJRZ01, title = {Automated Test and Oracle Generation for Smart-Card Applications}, author = {Duncan Clarke and Thierry Jéron and Vlad Rusu and Elena Zinovieva}, year = {2001}, url = {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 = {Smart Card Programming and Security, International Conference on Research in Smart Cards, E-smart 2001, Cannes, France, September 19-21, 2001, Proceedings}, editor = {Isabelle Attali and Thomas P. Jensen}, volume = {2140}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {3-540-42610-8}, } @article{ChevalNR24, title = {Formal definitions and proofs for partial (co)recursive functions}, author = {Horatiu Cheval and David Nowak and Vlad Rusu}, year = {2024}, doi = {10.1016/j.jlamp.2024.100999}, url = {https://doi.org/10.1016/j.jlamp.2024.100999}, researchr = {https://researchr.org/publication/ChevalNR24}, cites = {0}, citedby = {0}, journal = {J. Log. Algebr. Meth. Program.}, volume = {141}, pages = {100999}, } @inproceedings{ArusoaieLRSSR14, title = {Language Definitions as Rewrite Theories}, author = {Andrei Arusoaie and Dorel Lucanu and Vlad Rusu and Traian-Florin Serbanuta and Andrei Stefanescu and Grigore Rosu}, year = {2014}, doi = {10.1007/978-3-319-12904-4_5}, url = {http://dx.doi.org/10.1007/978-3-319-12904-4_5}, researchr = {https://researchr.org/publication/ArusoaieLRSSR14}, cites = {0}, citedby = {0}, pages = {97-112}, booktitle = {Rewriting Logic and Its Applications - 10th International Workshop, WRLA 2014, Held as a Satellite Event of ETAPS, Grenoble, France, April 5-6, 2014, Revised Selected Papers}, editor = {Santiago Escobar}, volume = {8663}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-319-12903-7}, } @inproceedings{RouxR94, title = {Verifying Time-bounded Properties for ELECTRE Reactive Programs with Stopwatch Automata}, author = {Olivier Roux and Vlad Rusu}, year = {1994}, tags = {reactive programming, program verification}, researchr = {https://researchr.org/publication/RouxR94}, cites = {0}, citedby = {0}, pages = {405-416}, booktitle = {Hybrid Systems II}, editor = {Panos J. Antsaklis and Wolf Kohn and Anil Nerode and Shankar Sastry}, volume = {999}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {3-540-60472-3}, } @article{CacheraJPR05, title = {Extracting a data flow analyser in constructive logic}, author = {David Cachera and Thomas P. Jensen and David Pichardie and Vlad Rusu}, year = {2005}, doi = {10.1016/j.tcs.2005.06.004}, url = {http://dx.doi.org/10.1016/j.tcs.2005.06.004}, 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 = {Theoretical Computer Science}, volume = {342}, number = {1}, pages = {56-78}, } @inproceedings{rusu:hal-01816798, title = {Proving Partial-Correctness and Invariance Properties of Transition-System Models}, author = {Vlad Rusu and Gilles Grimaud and Michaël Hauspie}, year = {2018}, month = {Aug}, 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}, address = {Guangzhou, China}, publisher = {IEEE Xplore}, } @inproceedings{RusuBJ00, title = {An Approach to Symbolic Test Generation}, author = {Vlad Rusu and Lydie du Bousquet and Thierry Jéron}, year = {2000}, url = {http://link.springer.de/link/service/series/0558/bibs/1945/19450338.htm}, tags = {control systems, reactive programming, testing, programming, systematic-approach}, researchr = {https://researchr.org/publication/RusuBJ00}, cites = {0}, citedby = {0}, pages = {338-357}, booktitle = {Integrated Formal Methods, Second International Conference, IFM 2000, Dagstuhl Castle, Germany, November 1-3, 2000, Proceedings}, editor = {Wolfgang Grieskamp and Thomas Santen and Bill Stoddart}, volume = {1945}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {3-540-41196-8}, } @proceedings{DBLP:journals-corr-abs-2209-09208, title = {Proceedings of the Sixth Working Formal Methods Symposium, FROM 2022, "Al. I. Cuza University", Iasi, Romania, 19-20 September, 2022}, year = {2022}, doi = {10.4204/EPTCS.369}, url = {https://doi.org/10.4204/EPTCS.369}, researchr = {https://researchr.org/publication/DBLP%3Ajournals-corr-abs-2209-09208}, cites = {0}, citedby = {0}, booktitle = {Proceedings of the Sixth Working Formal Methods Symposium, FROM 2022, "Al. I. Cuza University", Iasi, Romania, 19-20 September, 2022}, editor = {Vlad Rusu}, volume = {369}, series = {EPTCS}, } @proceedings{DBLP:conf-wrla-2018, 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}, 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 = {Vlad Rusu}, volume = {11152}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, isbn = {978-3-319-99839-8}, } @proceedings{DBLP:journals-corr-abs-1106-5962, title = {Proceedings Second International Workshop on Algebraic Methods in Model-based Software Engineering}, year = {2011}, doi = {10.4204/EPTCS.56}, 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 = {Francisco Duràn and Vlad Rusu}, volume = {56}, series = {Electronic Proceedings in Theoretical Computer Science}, }