Publications

𝕂 Definitions as Matching Logic Theories, Formally. FoSSaCS pp. 198-219, 2026. DOIDBLP

A unifying logical foundation for initial algebra semantics and induction. Theor. Comput. Sci. 1077 pp. 115981, 2026. DOIDBLP

Actors and Blockchains, Together. Concurrent Programming, Open Systems and Formal Methods pp. 215-236, 2026. DOIDBLP

Circular Induction. CoRR abs/2605.24968, 2026. DBLParXiv

FastSet: Parallel Claim Settlement. CoRR abs/2506.23395, 2025. DBLParXiv

A Logical Treatment of Finite Automata. TACAS pp. 350-369, 2024. DOIDBLPPDF

Capturing constrained constructor patterns in matching logic. J. Log. Algebraic Methods Program. 130 pp. 100810, 2023. DOIDBLP

Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier. Proc. ACM Program. Lang. 7 (OOPSLA1) pp. 56-84, 2023. DOIDBLPPDF

Model Checking Software - 28th International Symposium, SPIN 2022, Virtual Event, May 21, 2022, Proceedings. SPIN/Lecture Notes in Computer Science 13255, 2022. DOIDBLP

Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I. TACAS/Lecture Notes in Computer Science 13243, 2022. DOIDBLP

Language-parametric compiler validation with application to LLVM. ASPLOS pp. 1004-1019, 2021. DOIDBLP

Matching logic explained. J. Log. Algebraic Methods Program. 120 pp. 100638, 2021. DOIDBLPPDF

Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431). Dagstuhl Reports 11 (9) pp. 80-101, 2021. DOIDBLP

The K Vision for the Future of Programming Language Design and Analysis. Formal Methods in Outer Space pp. 3-9, 2021. DOIDBLP

Towards a Trustworthy Semantics-Based Language Framework via Proof Generation. CAV pp. 477-499, 2021. DOIDBLPPDF

A general approach to define binders using matching logic. Proc. ACM Program. Lang. 4 (ICFP) pp. 88:1-88:32, 2020. DOIDBLPPDF

Connecting Constrained Constructor Patterns and Matching Logic. WRLA pp. 19-37, 2020. DOIDBLPPDF

End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract. CAV pp. 151-164, 2020. DOIDBLP

Formal Design, Implementation and Verification of Blockchain Languages Using K (Invited Talk). FMBC@CAV pp. 1:1-1:1, 2020. DOIDBLP

Formal Semantics of Hybrid Automata. University of Illinois at Urbana-Champaign, 2020. PDF

Formalizing Correct-by-Construction Casper in Coq. IEEE ICBC pp. 1-3, 2020. DOIDBLP

Initial algebra semantics in matching logic. University of Illinois at Urbana-Champaign, 2020. PDF

Matching logic: the foundation of the K framework (invited talk). CPP pp. 1, 2020. DOIDBLP

Specification of the Giskard Consensus Protocol. CoRR abs/2010.02124, 2020. DBLParXiv

Towards a unified proof framework for automated fixpoint reasoning using matching logic. Proc. ACM Program. Lang. 4 (OOPSLA) pp. 161:1-161:29, 2020. DOIDBLPPDF

𝕂 - A Semantic Framework for Programming Languages and Formal Analysis. SETSS pp. 122-158, 2019. DOIDBLP

A complete formal semantics of x86-64 user-level instruction set architecture. PLDI pp. 1133-1148, 2019. DOIDBLPPDF

All-Path Reachability Logic. Log. Methods Comput. Sci. 15 (2), 2019. DOIDBLParXivPDF

Applicative Matching Logic: Semantics of K. University of Illinois at Urbana-Champaign, 2019. PDF

Dealing With C's Original Sin. IEEE Softw. 36 (5) pp. 24-28, 2019. DOIDBLP

First international Competition on Runtime Verification: rules, benchmarks, tools, and final results of CRV 2014. Int. J. Softw. Tools Technol. Transf. 21 (1) pp. 31-70, 2019. DOIDBLP

How effective are existing Java API specifications for finding bugs during runtime verification?. Autom. Softw. Eng. 26 (4) pp. 795-837, 2019. DOIDBLP

IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain. FM pp. 593-610, 2019. DOIDBLPPDF

Matching mu-Logic: Foundation of K Framework. Proceedings of the 8th Conference on Algebra and Coalgebra in Computer Science (CALCO'19), 2019. PDF

Matching mu-Logic: Foundation of K Framework (Invited Paper). CALCO pp. 1:1-1:4, 2019. DOIDBLP

Matching μ-Logic. LICS pp. 1-13, 2019. DOIDBLParXivPDF

Runtime Verification Past Experiences and Future Projections. Computing and Software Science pp. 532-562, 2019. DOIDBLP

Statistical Model Checking of RANDAO's Resilience to Pre-computed Reveal Strategies. FM Workshops pp. 337-349, 2019. DOIDBLP

Techniques for Evolution-Aware Runtime Verification. ICST pp. 300-311, 2019. DOIDBLPPDF

Towards a Verified Model of the Algorand Consensus Protocol in Coq. FM Workshops pp. 362-367, 2019. DOIDBLParXiv

SETSS'19 Lecture Notes on K. Engineering Trustworthy Software Systems, 2019. PDF

A formal verification tool for Ethereum VM bytecode. ESEC/SIGSOFT FSE pp. 912-915, 2018. DOIDBLPPDF

A Language-Independent Approach to Smart Contract Verification. ISoLA pp. 405-413, 2018. DOIDBLPPDF

A Language-Independent Program Verification Framework. ISoLA pp. 92-102, 2018. DOIDBLPPDF

Finite-trace linear temporal logic: coinductive completeness. Formal Methods Syst. Des. 53 (1) pp. 138-163, 2018. DOIDBLPPDF

IELE: An Intermediate-Level Blockchain Language Designed and Implemented Using Formal Semantics. University of Illinois, 2018. PDF

KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine. CSF pp. 204-217, 2018. DOIDBLP

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

P4K: A Formal Semantics of P4 and Applications. CoRR abs/1804.01468, 2018. DBLParXivPDF

Program Verification by Coinduction. ESOP pp. 589-618, 2018. DOIDBLPPDF

Runtime Verification - 17 Years Later. RV pp. 3-17, 2018. DOIDBLP

Open Problems and Challenges 2017. University of Illinois, 2017. PDF

Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017, Urbana, IL, USA, October 30 - November 03, 2017. ASE, 2017. DBLP

𝕂: A Semantic Framework for Programming Languages and Formal Analysis Tools. Dependable Software Systems Engineering pp. 186-206, 2017. DOIDBLPPDF

A language-independent proof system for full program equivalence. Formal Aspects Comput. 28 (3) pp. 469-497, 2016. DOIDBLPPDF

How good are the specs? a study of the bug-finding effectiveness of existing Java API specifications. ASE pp. 602-613, 2016. DOIDBLPPDF

Language definitions as rewrite theories. J. Log. Algebraic Methods Program. 85 (1) pp. 98-120, 2016. DOIDBLPPDF

Open Problems and Challenges 2016. University of Illinois, 2016. PDF

Runtime Verification at Work: A Tutorial. RV pp. 46-67, 2016. DOIDBLPPDF

RV-ECU: Maximum Assurance In-Vehicle Safety Monitoring. SAE 2016 World Congress and Exhibition, 2016. PDF

RV-Match: Practical Semantics-Based Program Analysis. CAV pp. 447-453, 2016. DOIDBLPPDF

Semantics-based program verifiers for all languages. OOPSLA pp. 74-91, 2016. DOIDBLPPDF

Towards a 𝕂ool Future. Theory and Practice of Formal Methods pp. 325-343, 2016. DOIDBLPPDF

Defining the undefinedness of C. PLDI pp. 336-345, 2015. DOIDBLPPDF

Evolution-Aware Monitoring-Oriented Programming. ICSE pp. 615-618, 2015. DOIDBLPPDF

From Rewriting Logic, to Programming Language Semantics, to Program Verification. Logic, Rewriting, and Concurrency pp. 598-616, 2015. DOIDBLPPDF

GPredict: Generic Predictive Concurrency Analysis. ICSE pp. 847-857, 2015. DOIDBLPPDF

K-Java: A Complete Semantics of Java. POPL pp. 445-456, 2015. DOIDBLPPDF

KJS: a complete formal semantics of JavaScript. PLDI pp. 346-356, 2015. DOIDBLPPDF

Matching Logic - Extended Abstract (Invited Talk). RTA pp. 5-21, 2015. DOIDBLP

Matching Logic --- Extended Abstract. Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA'15), 2015. PDF

RV-Android: Efficient Parametric Android Runtime Verification, a Brief Tutorial. RV pp. 342-357, 2015. DOIDBLPPDF

Term-generic logic. Theor. Comput. Sci. 577 pp. 1-24, 2015. DOIDBLPPDF

A Language-Independent Proof System for Mutual Program Equivalence. ICFEM pp. 75-90, 2014. DOIDBLPPDF

A Theoretical Foundation for Programming Languages Aggregation. WADT pp. 30-47, 2014. DOIDBLP

Behavioral Rewrite Systems and Behavioral Productivity. Specification, Algebra, and Software pp. 296-314, 2014. DOIDBLPPDF

Converting Parallel Code from Low-Level Abstractions to Higher-Level Abstractions. ECOOP 2014 – Object-Oriented Programming : 28th European Conference, Uppsala, Sweden, July 28-Aug 1, 2014. Proceedings, 2014. PDF

Matching Logic: A Logic for Structural Reasoning. University of Illinois, 2014. PDF

Maximal sound predictive race detection with control flow abstraction. PLDI pp. 337-348, 2014. DOIDBLPPDF

On the complexity of stream equality. J. Funct. Program. 24 (2-3) pp. 166-217, 2014. DOIDBLPPDF

Optimizing SYB is Easy!. Proceedings of the ACM SIGPLAN 2014 Workshop on Partial Evaluation and Program Manipulation, 2014. PDF

ROSRV: Runtime Verification for Robots. RV pp. 247-254, 2014. DOIDBLPPDF

RV-Monitor: Efficient Parametric Runtime Verification with Simultaneous Properties. RV pp. 285-300, 2014. DOIDBLPPDF

Symbolic Analysis Tools for CSP. Theoretical Aspects of Computing – ICTAC 2014, 2014. PDF

Efficient parametric runtime verification with deterministic string rewriting. ASE pp. 70-80, 2013. DOIDBLPPDF

EnforceMOP: a runtime property enforcement system for multithreaded programs. ISSTA pp. 156-166, 2013. DOIDBLPPDF

Low-Level Program Verification using Matching Logic Reachability. LOLA 2013: Syntax and Semantics of Low-Level Languages, 2013. PDF

Natural Proofs for Structure, Data, and Separation. Proceedings of the 34th Conference on Programming Language Design and Implementation (PLDI'13), 2013. PDF

One-Path Reachability Logic. LICS pp. 358-367, 2013. DOIDBLP

Proceedings of the 28th Symposium on Logic in Computer Science (LICS'13). Proceedings of the 28th Symposium on Logic in Computer Science (LICS'13), 2013. PDF

Specifying Languages and Verifying Programs with K. SYNASC pp. 28-31, 2013. DOIDBLPPDF

The rewriting logic semantics project: A progress report. Inf. Comput. 231 pp. 38-69, 2013. DOIDBLPPDF

A Formal Semantics of C with Applications. University of Illinois, 2012. PDF

A Truly Concurrent Semantics for the K Framework Based on Graph Transformations. ICGT pp. 294-310, 2012. DOIDBLPPDF

An executable formal semantics of C with applications. POPL pp. 533-544, 2012. DOIDBLPPDF

An overview of the MOP runtime verification framework. Int. J. Softw. Tools Technol. Transf. 14 (3) pp. 249-289, 2012. DOIDBLPPDF

Checking reachability using matching logic. OOPSLA pp. 555-574, 2012. DOIDBLPPDF

Efficient, Expressive, and Effective Runtime Verification. University of Illinois at Urbana-Champaign, 2012. PDF

Executing Formal Semantics with the K Tool. FM pp. 267-271, 2012. DOIDBLPPDF

Formal Techniques for Distributed Systems - Joint 14th IFIP WG 6.1 International Conference, FMOODS 2012 and 32nd IFIP WG 6.1 International Conference, FORTE 2012, Stockholm, Sweden, June 13-16, 2012. Proceedings. FMOODS/FORTE/Lecture Notes in Computer Science 7273, 2012. DOIDBLP

From Hoare Logic to Matching Logic Reachability. FM pp. 387-402, 2012. DOIDBLPPDF

Introduction to the special issue on runtime verification. Formal Methods Syst. Des. 41 (3) pp. 233-235, 2012. DOIDBLP

JavaMOP: Efficient parametric runtime monitoring framework. ICSE pp. 1427-1430, 2012. DOIDBLPPDF

K Framework Distilled. WRLA pp. 31-53, 2012. DOIDBLPPDF

Making Maude Definitions More Interactive. WRLA pp. 83-98, 2012. DOIDBLPPDF

Making Runtime Monitoring of Parametric Properties Practical. University of Illinois at Urbana-Champaign, 2012. PDF

Maximal Causal Models for Sequentially Consistent Systems. RV pp. 136-150, 2012. DOIDBLPPDF

On Safety Properties and Their Monitoring. Sci. Ann. Comput. Sci. 22 (2) pp. 327-365, 2012. DBLPPDF

Reachability Logic. University of Illinois, 2012. PDF

Recursive Proofs for Inductive Tree Data-Structures. Proceedings of the 39th Symposium on Principles of Programming Languages (POPL'12), 2012. PDF

Scalable Parametric Runtime Monitoring. University of Illinois at Urbana-Champaign, 2012. PDF

Security-policy monitoring and enforcement with JavaMOP. PLAS pp. 3, 2012. DOIDBLPPDF

Semantics and Algorithms for Parametric Monitoring. Log. Methods Comput. Sci. 8 (1), 2012. DOIDBLPPDF

Test-Case Reduction for C Compiler Bugs. Proceedings of the 33rd ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI'12), 2012. PDF

Towards a Unified Theory of Operational and Axiomatic Semantics. ICALP pp. 351-363, 2012. DOIDBLPPDF

Towards Categorizing and Formalizing the JDK API. University of Illinois at Urbana-Champaign, 2012. PDF

Abstract Semantics for K Module Composition. K pp. 127-149, 2011. DOIDBLPPDF

Garbage collection for monitoring parametric properties. PLDI pp. 415-424, 2011. DOIDBLPPDF

Improved multithreaded unit testing. SIGSOFT FSE pp. 223-233, 2011. DOIDBLPPDF

K Overview and SIMPLE Case Study. K pp. 3-56, 2011. DOIDBLPPDF

MatchC: A Matching Logic Reachability Verifier Using the K Framework. International K Workshop, 2011. PDF

Matching logic: a new program verification approach. ICSE pp. 868-871, 2011. DOIDBLPPDF

Matching Logic: A New Program Verification Approach (NIER Track). Proceedings of the 33rd International Conference on Software Engineering (ICSE'11), 2011. PDF

Mining parametric specifications. ICSE pp. 591-600, 2011. DOIDBLPPDF

The K Primer (version 3.3). K pp. 57-80, 2011. DOIDBLPPDF

Towards Semantics-Based WCET Analysis. Proceedings of the 11th Workshop on Worst-Case Execution-Time Analysis (WCET'11), 2011. PDF

A formal executable semantics of Verilog. MEMOCODE pp. 179-188, 2010. DOIDBLP

A Rewriting Approach to Concurrent Programming Language Design and Semantics. University of Illinois at Urbana-Champaign, 2010. PDF

A Rewriting Logic Semantics Approach to Modular Program Analysis. RTA pp. 151-160, 2010. DOIDBLP

An overview of the K semantic framework. J. Log. Algebraic Methods Program. 79 (6) pp. 397-434, 2010. DOIDBLP

Automating Coinduction with Case Analysis. ICFEM pp. 220-236, 2010. DOIDBLPPDF

Efficient monitoring of parametric context-free patterns. Autom. Softw. Eng. 17 (2) pp. 149-180, 2010. DOIDBLP

IMUnit: improved multithreaded unit testing. IWMSE@ICSE pp. 48-49, 2010. DOIDBLP

K-Maude: A Rewriting Based Tool for Semantics of Programming Languages. WRLA pp. 104-122, 2010. DOIDBLPPDF

Matching Logic: An Alternative to Hoare/Floyd Logic. AMAST pp. 142-162, 2010. DOIDBLPPDF

Maximal Causal Models for Sequentially Consistent Multithreaded Systems. University of Illinois, 2010. PDF

Runtime Verification - First International Conference, RV 2010, St. Julians, Malta, November 1-4, 2010. Proceedings. RV/Lecture Notes in Computer Science 6418, 2010. DOIDBLP

Runtime Verification with the RV System. RV pp. 136-152, 2010. DOIDBLPPDF

A rewriting logic approach to operational semantics. Inf. Comput. 207 (2) pp. 305-340, 2009. DOIDBLP

A semantic approach to interpolation. Theor. Comput. Sci. 410 (12-13) pp. 1109-1128, 2009. DOIDBLP

CIRC: A Behavioral Verification Tool Based on Circular Coinduction. CALCO pp. 433-442, 2009. DOIDBLP

Circular Coinduction with Special Contexts. ICFEM pp. 639-659, 2009. DOIDBLP

Circular Coinduction: A Proof Theoretical Foundation. CALCO pp. 127-144, 2009. DOIDBLP

Dependent advice: a general approach to optimizing history-based aspects. AOSD pp. 3-14, 2009. DOIDBLP

Efficient Formalism-Independent Monitoring of Parametric Properties. ASE pp. 383-394, 2009. DOIDBLP

Matching Logic --- Extended Report. University of Illinois at Urbana-Champaign, 2009. PDF

Parametric Trace Slicing and Monitoring. TACAS pp. 246-261, 2009. DOIDBLP

Proceedings of the Seventh International Workshop on Rewriting Logic and its Applications, WRLA 2008, Budapest, Hungary, March 29-30, 2008. WRLA/Electronic Notes in Theoretical Computer Science 238 (3), 2009. DBLP

Runtime Verification of C Memory Safety. RV pp. 132-151, 2009. DOIDBLP

A Rewriting Logic Approach to Static Checking of Units of Measurement in C. RULE pp. 51-67, 2008. DOIDBLP

A Rewriting Logic Approach to Type Inference. WADT pp. 135-151, 2008. DOIDBLP

Algebraic Methodology and Software Technology, 12th International Conference, AMAST 2008, Urbana, IL, USA, July 28-31, 2008, Proceedings. AMAST/Lecture Notes in Computer Science 5140, 2008. DOIDBLP

Defining and Executing P Systems with Structured Data in K. Workshop on Membrane Computing pp. 374-393, 2008. DOIDBLP

Hardware Runtime Monitoring for Dependable COTS-Based Real-Time Embedded Systems. RTSS pp. 481-491, 2008. DOIDBLP

jPredictor: a predictive runtime analysis tool for java. ICSE pp. 221-230, 2008. DOIDBLP

Preface. WRLA pp. 1-3, 2008. DOIDBLP

Runtime Verification, 02.01. - 06.01.2007. Runtime Verification/Dagstuhl Seminar Proceedings 07011, 2008. DBLP

Synthesizing Monitors for Safety Properties: This Time with Calls and Returns. RV pp. 51-68, 2008. DOIDBLP

Towards a Module System for K. WADT pp. 187-205, 2008. DOIDBLP

07011 Abstracts Collection -- Runtime Verification. Runtime Verification, 2007. DBLP

07011 Executive Summary -- Runtime Verification. Runtime Verification, 2007. DBLP

A rewriting approach to the design and evolution of object-oriented languages. OOPSLA Companion pp. 827-828, 2007. DOIDBLP

A Rewriting Logic Approach to Operational Semantics (Extended Abstract). SOS@LICS/ICALP pp. 125-141, 2007. DOIDBLP

An Effective Algorithm for the Membership Problem for Extended Regular Expressions. FoSSaCS pp. 332-345, 2007. DOIDBLP

An instrumentation technique for online analysis of multithreaded programs. Concurr. Comput. Pract. Exp. 19 (3) pp. 311-325, 2007. DOIDBLP

CIRC : A Circular Coinductive Prover. CALCO pp. 372-378, 2007. DOIDBLP

Editorial. High. Order Symb. Comput. 20 (1-2) pp. 1-2, 2007. DOIDBLP

KOOL: An Application of Rewriting Logic to Language Prototyping and Analysis. RTA pp. 246-256, 2007. DOIDBLP

Mop: an efficient and generic runtime verification framework. OOPSLA pp. 569-588, 2007. DOIDBLP

On Formal Analysis of OO Languages Using Rewriting Logic: Designing for Performance. FMOODS pp. 107-121, 2007. DOIDBLP

Parametric and Sliced Causality. CAV pp. 240-253, 2007. DOIDBLP

Regular Strategies as Proof Tactics for CIRC. WRS@RDP pp. 83-98, 2007. DOIDBLP

The rewriting logic semantics project. Theor. Comput. Sci. 373 (3) pp. 213-237, 2007. DOIDBLP

A Rewrite Framework for Language Definitions and for Generation of Efficient Interpreters. WRLA pp. 215-231, 2006. DOIDBLP

Allen Linear (Interval) Temporal Logic - Translation to LTL and Monitor Synthesis. CAV pp. 263-277, 2006. DOIDBLP

Complete Categorical Deduction for Satisfaction as Injectivity. Essays Dedicated to Joseph A. Goguen pp. 157-172, 2006. DOIDBLP

Computationally Equivalent Elimination of Conditions. RTA pp. 19-34, 2006. DOIDBLP

Decentralized runtime analysis of multithreaded applications. IPDPS, 2006. DOIDBLP

Equality of streams is a Pi0 over 2-complete problem. ICFP pp. 184-191, 2006. DOIDBLP

Formal Approaches to Software Testing and Runtime Verification, First Combined International Workshops, FATES 2006 and RV 2006, Seattle, WA, USA, August 15-16, 2006, Revised Selected Papers. FATES/RV/Lecture Notes in Computer Science 4262, 2006. DOIDBLP

Online efficient predictive safety analysis of multithreaded programs. Int. J. Softw. Tools Technol. Transf. 8 (3) pp. 248-260, 2006. DOIDBLP

Parametric and Termination-Sensitive Control Dependence. SAS pp. 387-404, 2006. DOIDBLP

Rewriting Logic Systems. WRLA pp. 233-247, 2006. DOIDBLP

Static Analysis to Enforce Safe Value Flow in Embedded Control Systems. DSN pp. 23-34, 2006. DOIDBLP

A Tree Based Router Search Engine Architecture with Single Port Memories. ISCA pp. 123-133, 2005. DOIDBLP

An Equational Specification for the Scheme Language. J. Univers. Comput. Sci. 11 (7) pp. 1327-1348, 2005. DOIDBLP

Behavioral Extensions of Institutions. CALCO pp. 331-347, 2005. DOIDBLP

Checking and Correcting Behaviors of Java Programs at Runtime with Java-MOP. RV@CAV pp. 3-20, 2005. DOIDBLP

Combining test case generation and runtime verification. Theor. Comput. Sci. 336 (2-3) pp. 209-234, 2005. DOIDBLP

Computational Logical Frameworks and Generic Program Analysis Technologies. VSTTE pp. 256-267, 2005. DOIDBLP

Detecting Errors in Multithreaded Programs by Generalized Predictive Analysis of Executions. FMOODS pp. 211-226, 2005. DOIDBLP

Efficient Monitoring of omega-Languages. CAV pp. 364-378, 2005. DOIDBLP

Foreword. Formal Methods Syst. Des. 27 (3) pp. 211-212, 2005. DOIDBLP

Formally Defining and Verifying Master/Slave Speculative Parallelization. FM pp. 123-138, 2005. DOIDBLP

Java-MOP: A Monitoring Oriented Programming Environment for Java. TACAS pp. 546-550, 2005. DOIDBLP

Monitoring Algorithms for Metric Temporal Logic. Proceedings of 5rd International Workshop on Runtime Verification (RV'05), 2005. PDF

Proceedings of the Fourth Workshop on Runtime Verification, RV@ETAPS 2004, Barcelona, Spain, April 3, 2004. RV@ETAPS/Electronic Notes in Theoretical Computer Science 113, 2005. DBLP

Rewriting-Based Techniques for Runtime Verification. Autom. Softw. Eng. 12 (2) pp. 151-197, 2005. DOIDBLPPDF

A Formal Monitoring-Based Framework for Software Development and Analysis. ICFEM pp. 357-372, 2004. DOIDBLP

An Overview of the Runtime Verification Tool Java PathExplorer. Formal Methods Syst. Des. 24 (2) pp. 189-215, 2004. DOIDBLP

Behavioral abstraction is hiding information. Theor. Comput. Sci. 327 (1-2) pp. 197-221, 2004. DOIDBLP

Composing Hidden Information Modules over Inclusive Institutions. Essays in Memory of Ole-Johan Dahl pp. 96-123, 2004. DOIDBLPPDF

Efficient Decentralized Monitoring of Safety in Distributed Systems. ICSE pp. 418-427, 2004. DOIDBLP

Efficient monitoring of safety properties. Int. J. Softw. Tools Technol. Transf. 6 (2) pp. 158-173, 2004. DOIDBLP

Extensional Theories and Rewriting. ICALP pp. 1066-1079, 2004. DOIDBLP

Foreword - Selected Papers from the First International Workshop on Runtime Verification held in Paris, July 2001 (RV'01). Formal Methods Syst. Des. 24 (2) pp. 99-100, 2004. DOIDBLP

Formal Analysis of Java Programs in JavaFAN. CAV pp. 501-505, 2004. DOIDBLP

Formal JVM Code Analysis in JavaFAN. AMAST pp. 132-147, 2004. DOIDBLP

From Conditional to Unconditional Rewriting. WADT pp. 218-233, 2004. DOIDBLP

Monitoring Algorithms for Metric Temporal Logic Specifications. RV@ETAPS pp. 145-162, 2004. DOIDBLP

Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools. IJCAR pp. 1-44, 2004. DOIDBLP

Certifying and Synthesizing Membership Equational Proofs. FME pp. 359-380, 2003. DOIDBLPPDF

Certifying Measurement Unit Safety Polic. ASE pp. 304-309, 2003. DOIDBLPPDF

Certifying Optimality of State Estimation Programs. CAV pp. 301-314, 2003. DOIDBLP

Experiments with Test Case Generation and Runtime Analysis. Abstract State Machines pp. 87-107, 2003. DOIDBLP

Generating Optimal Linear Temporal Logic Monitors by Coinduction. ASIAN pp. 260-275, 2003. DOIDBLPPDF

Generating Optimal Monitors for Extended Regular Expressions. RV@CAV pp. 226-245, 2003. DOIDBLPPDF

Inductive Behavioral Proofs by Unhiding. CMCS pp. 285-302, 2003. DOIDBLPPDF

Rule-Based Analysis of Dimensional Safety. RTA pp. 197-207, 2003. DOIDBLPPDF

Runtime safety analysis of multithreaded programs. ESEC / SIGSOFT FSE pp. 337-346, 2003. DOIDBLP

Testing Extended Regular Language Membership Incrementally by Rewriting. RTA pp. 499-514, 2003. DOIDBLPPDF

Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation. RV@CAV pp. 108-127, 2003. DOIDBLPPDF

CS322 - Programming Language Design: Lecture Notes. University of Illinois, 2003. PDF

A Total Approach to Partial Algebraic Specification. ICALP pp. 572-584, 2002. DOIDBLP

Axiomatizability in Inclusive Equational Logics. Math. Struct. Comput. Sci. 12 (5) pp. 541-563, 2002. DOIDBLP

Conditional Circular Coinductive Rewriting with Case Analysis. WADT pp. 216-232, 2002. DOIDBLP

Institution Morphisms. Formal Aspects Comput. 13 (3-5) pp. 274-307, 2002. DOIDBLP

On implementing behavioral rewriting. ACM SIGPLAN Workshop on Rule-Based Programming pp. 43-52, 2002. DOIDBLP

Runtime Verification 2002, RV 2002, FLoC Satellite Event, Copenhagen, Denmark, July 26, 2002. RV@FLoC/Electronic Notes in Theoretical Computer Science 70 (4), 2002. DBLP

Synthesizing Monitors for Safety Properties. TACAS pp. 342-356, 2002. DOIDBLPPDF

Towards Behavioral Maude: Behavioral Membership Equational Logic. CMCS pp. 197-253, 2002. DOIDBLP

Towards Certifying Domain-Specific Properties of Synthesized Code. ASE pp. 289-294, 2002. DOIDBLP

Certifying Domain-Specific Policies. ASE pp. 81-90, 2001. DOIDBLPPDF

Complete Categorical Equational Deduction. CSL pp. 528-538, 2001. DOIDBLP

Equational axiomatizability for coalgebra. Theor. Comput. Sci. 260 (1-2) pp. 229-247, 2001. DOIDBLP

Interpreting Abstract Interpretations in Membership Equational Logic. RULE@PLI pp. 271-285, 2001. DOIDBLPPDF

Monitoring Java Programs with Java PathExplorer. RV@CAV pp. 200-217, 2001. DOIDBLP

Monitoring Programs Using Rewriting. ASE pp. 135-143, 2001. DOIDBLPPDF

Synthesizing Dynamic Programming Algorithms from Linear Temporal Logic Formulae. Research Institute for Advanced Computer Science, 2001. PDF

Workshop on Runtime Verification, RV 2001, in connection with CAV 2001, Paris, France, July 23, 2001. RV@CAV/Electronic Notes in Theoretical Computer Science 55 (2), 2001. DBLP

Behavioral and Coinductive Rewriting. WRLA pp. 2-23, 2000. DOIDBLP

Circular Coinductive Rewriting. ASE pp. 123-132, 2000. DOIDBLP

Incompleteness of Behavioral Logics. CMCS pp. 61-79, 2000. DOIDBLP

On Equational Craig Interpolation. J. Univers. Comput. Sci. 6 (1) pp. 194-200, 2000. DOIDBLP

Weak Inclusion Systems: Part Two. J. Univers. Comput. Sci. 6 (1) pp. 5-21, 2000. DOIDBLP

A protocol for distributed cooperative work. WDS@FCT pp. 3, 1999. DOIDBLP

Hiding More of Hidden Algebra. World Congress on Formal Methods pp. 1704-1719, 1999. DOIDBLP

Kan Extensions of Institutions. J. Univers. Comput. Sci. 5 (8) pp. 482-493, 1999. DOIDBLP

A Birkhoff-like Axiomatizability Result for Hidden Algebra and Coalgebra. CMCS pp. 176-193, 1998. DOIDBLP

Hidden Congruent Deduction. FTP pp. 251-266, 1998. DOIDBLP

Distributed Cooperative Formal Methods Tools. ASE pp. 55-62, 1997. DOIDBLP

Weak Inclusion Systems. Math. Struct. Comput. Sci. 7 (2) pp. 195-206, 1997. DOIDBLP

The Institution of Order-Sorted Equational Logic. Bull. EATCS 53 pp. 250-255, 1994. DBLP