Grigore Rosu

According to our database1, Grigore Rosu authored at least 195 papers between 1994 and 2019.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2019
Runtime Verification Past Experiences and Future Projections.
Proceedings of the Computing and Software Science - State of the Art and Perspectives, 2019

First international Competition on Runtime Verification: rules, benchmarks, tools, and final results of CRV 2014.
STTT, 2019

Dealing With C's Original Sin.
IEEE Software, 2019

All-Path Reachability Logic.
Logical Methods in Computer Science, 2019

Towards a Verified Model of the Algorand Consensus Protocol in Coq.
CoRR, 2019

A complete formal semantics of x86-64 user-level instruction set architecture.
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

Matching μ-Logic.
Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, 2019

Techniques for Evolution-Aware Runtime Verification.
Proceedings of the 12th IEEE Conference on Software Testing, Validation and Verification, 2019

IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain.
Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019

2018
Finite-trace linear temporal logic: coinductive completeness.
Formal Methods in System Design, 2018

All-Path Reachability Logic.
CoRR, 2018

P4K: A Formal Semantics of P4 and Applications.
CoRR, 2018

A formal verification tool for Ethereum VM bytecode.
Proceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2018

Runtime Verification - 17 Years Later.
Proceedings of the Runtime Verification - 18th International Conference, 2018

Formal Design, Implementation and Verification of Blockchain Languages (Invited Talk).
Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, 2018

A Language-Independent Program Verification Framework.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Verification, 2018

A Language-Independent Approach to Smart Contract Verification.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice, 2018

Program Verification by Coinduction.
Proceedings of the Programming Languages and Systems, 2018

KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine.
Proceedings of the 31st IEEE Computer Security Foundations Symposium, 2018

2017
𝕂: A Semantic Framework for Programming Languages and Formal Analysis Tools.
Proceedings of the Dependable Software Systems Engineering, 2017

Matching Logic.
Logical Methods in Computer Science, 2017

Matching Logic.
CoRR, 2017

2016
Language definitions as rewrite theories.
J. Log. Algebr. Meth. Program., 2016

A language-independent proof system for full program equivalence.
Formal Asp. Comput., 2016

Finite-Trace Linear Temporal Logic: Coinductive Completeness.
Proceedings of the Runtime Verification - 16th International Conference, 2016

Runtime Verification at Work: A Tutorial.
Proceedings of the Runtime Verification - 16th International Conference, 2016

Semantics-based program verifiers for all languages.
Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, 2016

How good are the specs? a study of the bug-finding effectiveness of existing Java API specifications.
Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, 2016

RV-Match: Practical Semantics-Based Program Analysis.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016

Towards a \mathbb K K ool Future.
Proceedings of the Theory and Practice of Formal Methods, 2016

2015
Term-generic logic.
Theor. Comput. Sci., 2015

RV-Android: Efficient Parametric Android Runtime Verification, a Brief Tutorial.
Proceedings of the Runtime Verification - 6th International Conference, 2015

Matching Logic - Extended Abstract (Invited Talk).
Proceedings of the 26th International Conference on Rewriting Techniques and Applications, 2015

K-Java: A Complete Semantics of Java.
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

KJS: a complete formal semantics of JavaScript.
Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

Defining the undefinedness of C.
Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

Evolution-Aware Monitoring-Oriented Programming.
Proceedings of the 37th IEEE/ACM International Conference on Software Engineering, 2015

GPredict: Generic Predictive Concurrency Analysis.
Proceedings of the 37th IEEE/ACM International Conference on Software Engineering, 2015

From Rewriting Logic, to Programming Language Semantics, to Program Verification.
Proceedings of the Logic, Rewriting, and Concurrency, 2015

2014
On the complexity of stream equality.
J. Funct. Program., 2014

The K Primer (version 3.3).
Electr. Notes Theor. Comput. Sci., 2014

K Overview and SIMPLE Case Study.
Electr. Notes Theor. Comput. Sci., 2014

Abstract Semantics for K Module Composition.
Electr. Notes Theor. Comput. Sci., 2014

Language Definitions as Rewrite Theories.
Proceedings of the Rewriting Logic and Its Applications - 10th International Workshop, 2014

A Theoretical Foundation for Programming Languages Aggregation.
Proceedings of the Recent Trends in Algebraic Development Techniques, 2014

RV-Monitor: Efficient Parametric Runtime Verification with Simultaneous Properties.
Proceedings of the Runtime Verification - 5th International Conference, 2014

ROSRV: Runtime Verification for Robots.
Proceedings of the Runtime Verification - 5th International Conference, 2014

All-Path Reachability Logic.
Proceedings of the Rewriting and Typed Lambda Calculi - Joint International Conference, 2014

Maximal sound predictive race detection with control flow abstraction.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2014

A Language-Independent Proof System for Mutual Program Equivalence.
Proceedings of the Formal Methods and Software Engineering, 2014

Behavioral Rewrite Systems and Behavioral Productivity.
Proceedings of the Specification, Algebra, and Software, 2014

2013
The rewriting logic semantics project: A progress report.
Inf. Comput., 2013

Specifying Languages and Verifying Programs with K.
Proceedings of the 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2013

One-Path Reachability Logic.
Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013

Efficient parametric runtime verification with deterministic string rewriting.
Proceedings of the 2013 28th IEEE/ACM International Conference on Automated Software Engineering, 2013

EnforceMOP: a runtime property enforcement system for multithreaded programs.
Proceedings of the International Symposium on Software Testing and Analysis, 2013

2012
An overview of the MOP runtime verification framework.
STTT, 2012

Introduction to the special issue on runtime verification.
Formal Methods in System Design, 2012

A Rewriting Logic Approach to Static Checking of Units of Measurement in C.
Electr. Notes Theor. Comput. Sci., 2012

On Safety Properties and Their Monitoring.
Sci. Ann. Comp. Sci., 2012

Semantics and Algorithms for Parametric Monitoring
Logical Methods in Computer Science, 2012

K Framework Distilled.
Proceedings of the Rewriting Logic and Its Applications - 9th International Workshop, 2012

Making Maude Definitions More Interactive.
Proceedings of the Rewriting Logic and Its Applications - 9th International Workshop, 2012

Maximal Causal Models for Sequentially Consistent Systems.
Proceedings of the Runtime Verification, Third International Conference, 2012

An executable formal semantics of C with applications.
Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

Security-policy monitoring and enforcement with JavaMOP.
Proceedings of the 2012 Workshop on Programming Languages and Analysis for Security, 2012

Checking reachability using matching logic.
Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2012

JavaMOP: Efficient parametric runtime monitoring framework.
Proceedings of the 34th International Conference on Software Engineering, 2012

Towards a Unified Theory of Operational and Axiomatic Semantics.
Proceedings of the Automata, Languages, and Programming - 39th International Colloquium, 2012

A Truly Concurrent Semantics for the K Framework Based on Graph Transformations.
Proceedings of the Graph Transformations - 6th International Conference, 2012

From Hoare Logic to Matching Logic Reachability.
Proceedings of the FM 2012: Formal Methods, 2012

Executing Formal Semantics with the K Tool.
Proceedings of the FM 2012: Formal Methods, 2012

2011
Improved multithreaded unit testing.
Proceedings of the SIGSOFT/FSE'11 19th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-19) and ESEC'11: 13th European Software Engineering Conference (ESEC-13), 2011

Garbage collection for monitoring parametric properties.
Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, 2011

Matching logic: a new program verification approach.
Proceedings of the 33rd International Conference on Software Engineering, 2011

Mining parametric specifications.
Proceedings of the 33rd International Conference on Software Engineering, 2011

The Rewriting Logic Semantics Project: A Progress Report.
Proceedings of the Fundamentals of Computation Theory - 18th International Symposium, 2011

2010
An overview of the K semantic framework.
J. Log. Algebr. Program., 2010

Efficient monitoring of parametric context-free patterns.
Autom. Softw. Eng., 2010

K-Maude: A Rewriting Based Tool for Semantics of Programming Languages.
Proceedings of the Rewriting Logic and Its Applications - 8th International Workshop, 2010

Runtime Verification with the RV System.
Proceedings of the Runtime Verification - First International Conference, 2010

A Rewriting Logic Semantics Approach to Modular Program Analysis.
Proceedings of the 21st International Conference on Rewriting Techniques and Applications, 2010

A formal executable semantics of Verilog.
Proceedings of the 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), 2010

Automating Coinduction with Case Analysis.
Proceedings of the Formal Methods and Software Engineering, 2010

Matching Logic: An Alternative to Hoare/Floyd Logic.
Proceedings of the Algebraic Methodology and Software Technology, 2010

2009
A semantic approach to interpolation.
Theor. Comput. Sci., 2009

A rewriting logic approach to operational semantics.
Inf. Comput., 2009

Preface.
Electr. Notes Theor. Comput. Sci., 2009

Parametric Trace Slicing and Monitoring.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2009

Runtime Verification of C Memory Safety.
Proceedings of the Runtime Verification, 9th International Workshop, 2009

Efficient Formalism-Independent Monitoring of Parametric Properties.
Proceedings of the ASE 2009, 2009

Circular Coinduction with Special Contexts.
Proceedings of the Formal Methods and Software Engineering, 2009

Circular Coinduction: A Proof Theoretical Foundation.
Proceedings of the Algebra and Coalgebra in Computer Science, 2009

CIRC: A Behavioral Verification Tool Based on Circular Coinduction.
Proceedings of the Algebra and Coalgebra in Computer Science, 2009

Dependent advice: a general approach to optimizing history-based aspects.
Proceedings of the 8th International Conference on Aspect-Oriented Software Development, 2009

2008
Regular Strategies as Proof Tactics for CIRC.
Electr. Notes Theor. Comput. Sci., 2008

Term-Generic Logic.
Proceedings of the Recent Trends in Algebraic Development Techniques, 2008

Towards a Module System for K.
Proceedings of the Recent Trends in Algebraic Development Techniques, 2008

A Rewriting Logic Approach to Type Inference.
Proceedings of the Recent Trends in Algebraic Development Techniques, 2008

Synthesizing Monitors for Safety Properties: This Time with Calls and Returns.
Proceedings of the Runtime Verification, 8th International Workshop, 2008

Hardware Runtime Monitoring for Dependable COTS-Based Real-Time Embedded Systems.
Proceedings of the 29th IEEE Real-Time Systems Symposium, 2008

Defining and Executing P Systems with Structured Data in K.
Proceedings of the Membrane Computing - 9th International Workshop, 2008

Efficient Monitoring of Parametric Context-Free Patterns.
Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008), 2008

jPredictor: a predictive runtime analysis tool for java.
Proceedings of the 30th International Conference on Software Engineering (ICSE 2008), 2008

2007
The rewriting logic semantics project.
Theor. Comput. Sci., 2007

Editorial.
Higher-Order and Symbolic Computation, 2007

A Rewriting Logic Approach to Operational Semantics (Extended Abstract).
Electr. Notes Theor. Comput. Sci., 2007

A Rewrite Framework for Language Definitions and for Generation of Efficient Interpreters.
Electr. Notes Theor. Comput. Sci., 2007

Rewriting Logic Systems.
Electr. Notes Theor. Comput. Sci., 2007

An instrumentation technique for online analysis of multithreaded programs.
Concurrency and Computation: Practice and Experience, 2007

KOOL: An Application of Rewriting Logic to Language Prototyping and Analysis.
Proceedings of the Term Rewriting and Applications, 18th International Conference, 2007

A rewriting approach to the design and evolution of object-oriented languages.
Proceedings of the Companion to the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2007

Mop: an efficient and generic runtime verification framework.
Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2007

An Effective Algorithm for the Membership Problem for Extended Regular Expressions.
Proceedings of the Foundations of Software Science and Computational Structures, 2007

On Formal Analysis of OO Languages Using Rewriting Logic: Designing for Performance.
Proceedings of the Formal Methods for Open Object-Based Distributed Systems, 2007

07011 Abstracts Collection -- Runtime Verification.
Proceedings of the Runtime Verification, 02.01. - 06.01.2007, 2007

07011 Executive Summary -- Runtime Verification.
Proceedings of the Runtime Verification, 02.01. - 06.01.2007, 2007

Parametric and Sliced Causality.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

CIRC : A Circular Coinductive Prover.
Proceedings of the Algebra and Coalgebra in Computer Science, 2007

2006
Online efficient predictive safety analysis of multithreaded programs.
STTT, 2006

The Rewriting Logic Semantics Project.
Electr. Notes Theor. Comput. Sci., 2006

Checking and Correcting Behaviors of Java Programs at Runtime with Java-MOP.
Electr. Notes Theor. Comput. Sci., 2006

Parametric and Termination-Sensitive Control Dependence.
Proceedings of the Static Analysis, 13th International Symposium, 2006

Computationally Equivalent Elimination of Conditions.
Proceedings of the Term Rewriting and Applications, 17th International Conference, 2006

Decentralized runtime analysis of multithreaded applications.
Proceedings of the 20th International Parallel and Distributed Processing Symposium (IPDPS 2006), 2006

Equality of streams is a Pi0 over 2-complete problem.
Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, 2006

A Semantic Approach to Interpolation.
Proceedings of the Foundations of Software Science and Computation Structures, 2006

Static Analysis to Enforce Safe Value Flow in Embedded Control Systems.
Proceedings of the 2006 International Conference on Dependable Systems and Networks (DSN 2006), 2006

Allen Linear (Interval) Temporal Logic - Translation to LTL and Monitor Synthesis.
Proceedings of the Computer Aided Verification, 18th International Conference, 2006

Complete Categorical Deduction for Satisfaction as Injectivity.
Proceedings of the Algebra, Meaning, and Computation, 2006

2005
Combining test case generation and runtime verification.
Theor. Comput. Sci., 2005

An Equational Specification for the Scheme Language.
J. UCS, 2005

Foreword.
Formal Methods in System Design, 2005

Monitoring Algorithms for Metric Temporal Logic Specifications.
Electr. Notes Theor. Comput. Sci., 2005

Rewriting-Based Techniques for Runtime Verification.
Autom. Softw. Eng., 2005

Computational Logical Frameworks and Generic Program Analysis Technologies.
Proceedings of the Verified Software: Theories, 2005

Java-MOP: A Monitoring Oriented Programming Environment for Java.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

A Tree Based Router Search Engine Architecture with Single Port Memories.
Proceedings of the 32st International Symposium on Computer Architecture (ISCA 2005), 2005

Detecting Errors in Multithreaded Programs by Generalized Predictive Analysis of Executions.
Proceedings of the Formal Methods for Open Object-Based Distributed Systems, 2005

Formally Defining and Verifying Master/Slave Speculative Parallelization.
Proceedings of the FM 2005: Formal Methods, 2005

Efficient Monitoring of omega-Languages.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

Behavioral Extensions of Institutions.
Proceedings of the Algebra and Coalgebra in Computer Science: First International Conference, 2005

2004
Behavioral abstraction is hiding information.
Theor. Comput. Sci., 2004

Efficient monitoring of safety properties.
STTT, 2004

An Overview of the Runtime Verification Tool Java PathExplorer.
Formal Methods in System Design, 2004

Foreword - Selected Papers from the First International Workshop on Runtime Verification held in Paris, July 2001 (RV'01).
Formal Methods in System Design, 2004

From Conditional to Unconditional Rewriting.
Proceedings of the Recent Trends in Algebraic Development Techniques, 2004

Online Efficient Predictive Safety Analysis of Multithreaded Programs.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

An Instrumentation Technique for Online Analysis of Multithreaded Programs.
Proceedings of the 18th International Parallel and Distributed Processing Symposium (IPDPS 2004), 2004

Efficient Decentralized Monitoring of Safety in Distributed Systems.
Proceedings of the 26th International Conference on Software Engineering (ICSE 2004), 2004

A Formal Monitoring-Based Framework for Software Development and Analysis.
Proceedings of the Formal Methods and Software Engineering, 2004

Extensional Theories and Rewriting.
Proceedings of the Automata, Languages and Programming: 31st International Colloquium, 2004

Formal Analysis of Java Programs in JavaFAN.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004

Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools.
Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

Composing Hidden Information Modules over Inclusive Institutions.
Proceedings of the From Object-Orientation to Formal Methods, 2004

Formal JVM Code Analysis in JavaFAN.
Proceedings of the Algebraic Methodology and Software Technology, 2004

2003
Generating Optimal Monitors for Extended Regular Expressions.
Electr. Notes Theor. Comput. Sci., 2003

Inductive Behavioral Proofs by Unhiding.
Electr. Notes Theor. Comput. Sci., 2003

Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation.
Electr. Notes Theor. Comput. Sci., 2003

Runtime safety analysis of multithreaded programs.
Proceedings of the 11th ACM SIGSOFT Symposium on Foundations of Software Engineering 2003 held jointly with 9th European Software Engineering Conference, 2003

Testing Extended Regular Language Membership Incrementally by Rewriting.
Proceedings of the Rewriting Techniques and Applications, 14th International Conference, 2003

Rule-Based Analysis of Dimensional Safety.
Proceedings of the Rewriting Techniques and Applications, 14th International Conference, 2003

Certifying Measurement Unit Safety Polic.
Proceedings of the 18th IEEE International Conference on Automated Software Engineering (ASE 2003), 2003

Certifying and Synthesizing Membership Equational Proofs.
Proceedings of the FME 2003: Formal Methods, 2003

Certifying Optimality of State Estimation Programs.
Proceedings of the Computer Aided Verification, 15th International Conference, 2003

Experiments with Test Case Generation and Runtime Analysis.
Proceedings of the Abstract State Machines, 2003

Generating Optimal Linear Temporal Logic Monitors by Coinduction.
Proceedings of the Advances in Computing Science, 2003

2002
Axiomatizability in Inclusive Equational Logics.
Mathematical Structures in Computer Science, 2002

Institution Morphisms.
Formal Asp. Comput., 2002

Towards Behavioral Maude: Behavioral Membership Equational Logic.
Electr. Notes Theor. Comput. Sci., 2002

Preface.
Electr. Notes Theor. Comput. Sci., 2002

Conditional Circular Coinductive Rewriting with Case Analysis.
Proceedings of the Recent Trends in Algebraic Development Techniques, 2002

Synthesizing Monitors for Safety Properties.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2002

On implementing behavioral rewriting.
Proceedings of the 2002 ACM SIGPLAN Workshop on Rule-Based Programming, 2002

Towards Certifying Domain-Specific Properties of Synthesized Code.
Proceedings of the 17th IEEE International Conference on Automated Software Engineering (ASE 2002), 2002

A Total Approach to Partial Algebraic Specification.
Proceedings of the Automata, Languages and Programming, 29th International Colloquium, 2002

2001
Equational axiomatizability for coalgebra.
Theor. Comput. Sci., 2001

Interpreting Abstract Interpretations in Membership Equational Logic.
Electr. Notes Theor. Comput. Sci., 2001

Monitoring Java Programs with Java PathExplorer.
Electr. Notes Theor. Comput. Sci., 2001

Certifying Domain-Specific Policies.
Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE 2001), 2001

Monitoring Programs Using Rewriting.
Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE 2001), 2001

Complete Categorical Equational Deduction.
Proceedings of the Computer Science Logic, 15th International Workshop, 2001

2000
On Equational Craig Interpolation.
J. UCS, 2000

Weak Inclusion Systems: Part Two.
J. UCS, 2000

Behavioral and Coinductive Rewriting.
Electr. Notes Theor. Comput. Sci., 2000

Incompleteness of Behavioral Logics.
Electr. Notes Theor. Comput. Sci., 2000

Circular Coinductive Rewriting.
Proceedings of the Fifteenth IEEE International Conference on Automated Software Engineering, 2000

1999
Kan Extensions of Institutions.
J. UCS, 1999

A protocol for distributed cooperative work.
Electr. Notes Theor. Comput. Sci., 1999

Hiding More of Hidden Algebra.
Proceedings of the FM'99 - Formal Methods, 1999

1998
A Birkhoff-like Axiomatizability Result for Hidden Algebra and Coalgebra.
Electr. Notes Theor. Comput. Sci., 1998

Hidden Congruent Deduction.
Proceedings of the Automated Deduction in Classical and Non-Classical Logics, 1998

1997
Weak Inclusion Systems.
Mathematical Structures in Computer Science, 1997

Distributed Cooperative Formal Methods Tools.
Proceedings of the 1997 International Conference on Automated Software Engineering, 1997

1994
The Institution of Order-Sorted Equational Logic.
Bulletin of the EATCS, 1994


  Loading...