A Certified Procedure for RL Verification (SYNASC 2017 post-proceedings, to appear in IEEE Conference Publishing Service ) David Nowak and Vlad Rusu and Andrei Arusoaie and Dorel Lucanu BIB
A Comparison of Open-Source Static Analysis Tools for Vulnerability Detection in C/C++ Code (SYNASC 2017 post-proceedings, to appear) Dragos Gavrilut and Vlad Craciun and Stefan Ciobaca and Andrei Arusoaie and Dorel Lucanu PDF BIB
A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems Stefan Ciobaca and Dorel Lucanu PDF BIB
A Certified Procedure for RL Verification (SYNASC 2017 pre-proceedings) David Nowak and Vlad Rusu and Andrei Arusoaie and Dorel Lucanu PDF BIB
Executing and verifying higher-order functional-imperative programs in Maude. Vlad Rusu and Andrei Arusoaie ScienceDirect BIB
A generic framework for symbolic execution: A coinductive approach Vlad Rusu and Andrei Arusoaie and Dorel Lucanu ScienceDirect BIB
A Comparison of Open-Source Static Analysis Tools for Vulnerability Detection in C/C++ Code (SYNASC 2017 pre-proceedings) Dragos Gavrilut and Vlad Craciun and Stefan Ciobaca and Andrei Arusoaie and Dorel Lucanu PDF BIB
Language definitions as rewrite theories Andrei Stefanescu and Vlad Rusu and Traian Serbanuta and Grigore Rosu and Andrei Arusoaie and Dorel Lucanu Elsevier BIB
Symbolic execution based on language transformation Vlad Rusu and Andrei Arusoaie and Dorel Lucanu DOI BIB
Symbolic execution based on language transformation Vlad Rusu and Andrei Arusoaie and Dorel Lucanu Elsevier BIB
Verifying Reachability-Logic Properties on Rewriting-Logic Specifications David Nowak and Vlad Rusu and Andrei Arusoaie and Dorel Lucanu LRC BIB
Verifying Reachability-Logic Properties on Rewriting-Logic Specifications (Extended Version) David Nowak and Vlad Rusu and Andrei Arusoaie and Dorel Lucanu TR15-01 BIB
Model checking recursive programs interacting via the heap Frank de Boer and Jurriann Rot and Marcello Bonsangue and Irina Asavoae and Dorel Lucanu Elsevier BIB
A Language-Independent Proof System for Mutual Program Equivalence Stefan Ciobaca and Vlad Rusu and Grigore Rosu and Dorel Lucanu ICFEM2014 BIB
All-Path Reachability Logic Andrei Stefanescu and Brandon Moore and Stefan Ciobaca and Radu Mereuta and Traian Serbanuta and Grigore Rosu PDF BIB
Language Definitions as Rewrite Theories Andrei Stefanescu and Vlad Rusu and Traian Serbanuta and Grigore Rosu and Andrei Arusoaie and Dorel Lucanu WRLA14 BIB
On the Complexity of Stream Equality Joerg Endrullis and Rena Bakhshi and Dimitri Hendriks and Grigore Rosu FSL BIB
On Automation of OTS/CafeOBJ Method Kokichi Futatsugi and Kazuhiro Ogata and Daniel Gaina and Dorel Lucanu Futatsugi Festschrift 2014 BIB
Behavioral Rewrite Systems and Behavioral Productivity Grigore Rosu and Dorel Lucanu PDF Futatsugi Festschrift 2014 BIB
The K Primer (version 3.2) David Lazar and Chucky Ellison and Traian Serbanuta and Grigore Rosu and Andrei Arusoaie and Dorel Lucanu K11 BIB
Rewriting Semantics and Analysis of Concurrency Features for a C-like Language Traian Serbanuta K11 BIB
One-Path Reachability Logic Andrei Stefanescu and Brandon Moore and Stefan Ciobaca and Grigore Rosu PDF BIB
A Generic Framework for Symbolic Execution Vlad Rusu and Andrei Arusoaie and Dorel Lucanu PDF SLE2013 BIB
Language-Independent Program Verification Using Symbolic Execution Vlad Rusu and Andrei Arusoaie and Dorel Lucanu INRIA RR-8369 BIB
Symbolic Execution in the K Framework: Support and Applications Vlad Rusu and Andrei Arusoaie and Dorel Lucanu PAS 2013 BIB
Programming Language Semantics using K — true concurrency through term-graph rewriting — Traian Serbanuta TERMGRAPH BIB
One-Path Reachability Logic Andrei Stefanescu and Brandon Moore and Stefan Ciobaca and Grigore Rosu One-Path Reachability Logic BIB
Automatic equivalence proofs for non-deterministic coalgebras Jan Rutten and Alexandra Silva and Marcello Bonsangue and Georgiana Caltais and Eugen Goriac and Dorel Lucanu SCP BIB
Maximal Causal Models for Sequentially Consistent Systems Feng Chen and Traian Serbanuta and Grigore Rosu PDF RV BIB
A Truly Concurrent Semantics for the K Framework Based on Graph Transformations Traian Serbanuta and Grigore Rosu PDF ICGT BIB
Bounded Model Checking of Recursive Programs with Pointers in K Frank de Boer and Jurriann Rot and Marcello Bonsangue and Irina Asavoae and Dorel Lucanu WADT2012 BIB
Checking Reachability using Matching Logic Andrei Stefanescu and Grigore Rosu See it on FSL-UIUC web page BIB
Interacting via the Heap in the Presence of Recursion Frank de Boer and Jurriann Rot and Marcello Bonsangue and Irina Asavoae and Dorel Lucanu ICE2012 BIB
A Generic Approach to Symbolic Execution Vlad Rusu and Andrei Arusoaie and Dorel Lucanu INRIA RR-8189 BIB
Executing Formal Semantics with the K Tool David Lazar and Chucky Ellison and Radu Mereuta and Traian Serbanuta and Grigore Rosu and Andrei Arusoaie and Dorel Lucanu FM12 BIB
Automating Abstract Syntax Tree construction for Context Free Grammars Daniel Ionut Vicol and Andrei Arusoaie SYNASC BIB
Towards a Unified Theory of Operational and Axiomatic Semantics Andrei Stefanescu and Grigore Rosu See it on FSL-UIUC web page BIB
From Hoare Logic to Matching Logic Reachability Andrei Stefanescu and Grigore Rosu See it on FSL-UIUC web page BIB
Making Maude Definitions more Interactive Chucky Ellison and Traian Serbanuta and Grigore Rosu and Andrei Arusoaie PDF WRLA2012 BIB
A K-Based Formal Framework for Domain-Specific Modelling Languages Vlad Rusu and Dorel Lucanu FoVeOOS BIB
Using the Executable Semantics for CFG Extraction and Unfolding Mihail Asavoae and Irina Asavoae PDF aa-synasc11 BIB
K Semantics for OCL – a Proposal for a Formal Definition for OCL Vlad Rusu and Dorel Lucanu PDF K11 BIB
A decision procedure for bisimilarity of generalized regular expressions Jan Rutten and Alexandra Silva and Marcello Bonsangue and Georgiana Caltais and Eugen Goriac and Dorel Lucanu SBMF 2010 BIB
Collecting Semantics under Predicate Abstraction in the K Framework Mihail Asavoae and Irina Asavoae PDF aaWRLA10 BIB
Automating Coinduction with Case Analysis Grigore Rosu and Eugen Goriac and Dorel Lucanu ICFEM2010 BIB
Path Directed Symbolic Execution in the K Framework Mihail Asavoae and Irina Asavoae and Dorel Lucanu PDF SYNASC BIB
Model-based Testing and Analysis of Coordinated Components Gabriel Ciobanu and Dorel Lucanu ECEASST BIB
Automated Proving of the Behavioral Attributes Georgiana Caltais and Gheorghe Grigoras and Eugen Goriac and Dorel Lucanu BCI BIB
CIRC : A Behavioral Verification Tool based on Circular Coinduction Grigore Rosu and Georgiana Caltais and Eugen Goriac and Dorel Lucanu CALCO BIB
Strategy-Based Rewrite Semantics for Membrane Systems Preserves Maximal Concurrency of Evolution Rule Actions Dorel Lucanu ENTCS BIB
Patterns for Maude Metalanguage Applications Oana Andrei and Georgiana Caltais and Gheorghe Grigoras and Eugen Goriac and Dorel Lucanu WRLA 2008 BIB
A Rewrite Stack Machine for ROC! Georgiana Caltais and Gheorghe Grigoras and Eugen Goriac and Dorel Lucanu SYNASC BIB
Regular Strategies as Proof Tactics for CIRC Grigore Rosu and Gheorghe Grigoras and Dorel Lucanu ENTCS BIB
A rewriting logic framework for operational semantics of membrane systems Gabriel Ciobanu and Oana Andrei and Dorel Lucanu TCS BIB
Operational Semantics and Rewriting Logic in Membrane Computing Gabriel Ciobanu and Oana Andrei and Dorel Lucanu ENTCS BIB
Semantic Web Languages – Towards an Institutional Perspective Jing Song Dong and Y.F. Li and Dorel Lucanu PDF Springer BIB
Expressing Control Mechanisms of Membranes by Rewriting Strategies. Gabriel Ciobanu and Oana Andrei and Dorel Lucanu WMC BIB
Structural Operational Semantics of P Systems Gabriel Ciobanu and Oana Andrei and Dorel Lucanu WMC BIB
Institution Morphisms for Relating OWL and Z Jing Song Dong and Y.F. Li and Dorel Lucanu PDF SEKE BIB
Specification of Coordinated Objects and Verification of Their Temporal Properties Gabriel Ciobanu and Mihai Danes and Dorel Lucanu SYNASC BIB
Soundness proof of Z semantics of OWL using institutions Jing Song Dong and Y.F. Li and Dorel Lucanu WWW BIB
Specification and Verification of Synchronizing Concurrent Objects Gabriel Ciobanu and Dorel Lucanu IFM BIB
Specification and Verification of Synchronizing Concurrent Objects Gabriel Ciobanu and Dorel Lucanu IFM2004 BIB
Model Checking for Object Specifications in Hidden Algebra Gabriel Ciobanu and Dorel Lucanu VMCAI BIB
Mixed Relations as Enriched Semiringal Categories Radu Grosu and Gheorghe Stefanescu and Dorel Lucanu JUCS BIB
