If you made any changes in Pure, your changes will be visible here soon.

Research Output 1997 2019

Filter
Article
2019

All-Path reachability logic

Ştefanescu, A., Ciobâcă, S., Mereuta, R., Moore, B. M., Roşu, G. & şerbănuţă, T. F., Jan 1 2019, In : Logical Methods in Computer Science. 15, 2, p. 5:1-5:23

Research output: Contribution to journalArticle

Reachability
Proof System
Semantics
Logic
Path

Dealing with C's Original Sin

Hathhorn, C. & Rosu, G., Sep 1 2019, In : IEEE Software. 36, 5, p. 24-28 5 p., 8802866.

Research output: Contribution to journalArticle

UNIX
Computer operating systems

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

Bartocci, E., Falcone, Y., Bonakdarpour, B., Colombo, C., Decker, N., Havelund, K., Joshi, Y., Klaedtke, F., Milewicz, R., Reger, G., Rosu, G., Signoles, J., Thoma, D., Zalinescu, E. & Zhang, Y., Feb 6 2019, In : International Journal on Software Tools for Technology Transfer. 21, 1, p. 31-70 40 p.

Research output: Contribution to journalArticle

Monitoring
Satellites

How effective are existing Java API specifications for finding bugs during runtime verification?

Legunsen, O., Al Awar, N., Xu, X., Hassan, W. U., Roşu, G. & Marinov, D., Dec 1 2019, In : Automated Software Engineering. 26, 4, p. 795-837 43 p.

Research output: Contribution to journalArticle

Application programming interfaces (API)
Specifications
Software engineering
Monitoring
Testing
2018

Finite-trace linear temporal logic: coinductive completeness

Rosu, G., Aug 1 2018, In : Formal Methods in System Design. 53, 1, p. 138-163 26 p.

Research output: Contribution to journalArticle

Linear Temporal Logic
Temporal logic
Completeness
Trace
Proof System
2017

Matching logic

Rosu, G., Jan 1 2017, In : Logical Methods in Computer Science. 13, 4, 28.

Research output: Contribution to journalArticle

Pattern matching
First-order Logic
Acoustic waves
Logic
Surface mount technology
2016

A language-independent proof system for full program equivalence

Ciobâcă, Ş., Lucanu, D., Rusu, V. & Roşu, G., May 1 2016, In : Formal Aspects of Computing. 28, 3, p. 469-497 29 p.

Research output: Contribution to journalArticle

Proof System
Semantics
Equivalence
Acoustic waves
Terminate

Language definitions as rewrite theories

Rusu, V., Lucanu, D., Şerbənuţə, T. F., Arusoaie, A., Ştefənescu, A. & Roşu, G., Jan 2016, In : Journal of Logical and Algebraic Methods in Programming. 85, 1, p. 98-120 23 p.

Research output: Contribution to journalArticle

Maude
Program compilers
Computer programming languages
Semantics
Engines
2015

Defining the undefinedness of C

Hathhorn, C., Ellison, C. & Rosu, G., Jun 2015, In : ACM SIGPLAN Notices. 50, 6, p. 336-345 10 p.

Research output: Contribution to journalArticle

Semantics

K-Java: A complete semantics of Java

Bogdənaş, D. & Rosu, G., Jan 2015, In : ACM SIGPLAN Notices. 50, 1, p. 445-456 12 p.

Research output: Contribution to journalArticle

Semantics

KJS: A complete formal semantics of javascript

Park, D., Stefanescu, A. & Rosu, G., Jun 2015, In : ACM SIGPLAN Notices. 50, 6, p. 346-356 11 p.

Research output: Contribution to journalArticle

Semantics
Acceptance tests
Engines

Term-generic logic

Popescu, A. & Rosu, G., Jan 1 2015, In : Theoretical Computer Science. 577, 1, p. 1-24 24 p.

Research output: Contribution to journalArticle

Logic
Term
Calculus
First-order Logic
Model
2014

Abstract semantics for K module composition

Girlea, C. & Rosu, G., Jun 10 2014, In : Electronic Notes in Theoretical Computer Science. 304, p. 127-149 23 p.

Research output: Contribution to journalArticle

Semantics
Module
Chemical analysis
Modularization
Model Theory
Productivity
Rewriting
Termination
Behavioral Approach
Binary trees

K overview and SIMPLE case study

Rosu, G. & Şerbǎnuţǎ, T. F., Jun 10 2014, In : Electronic Notes in Theoretical Computer Science. 304, p. 3-56 54 p.

Research output: Contribution to journalArticle

Computer programming languages
Programming Languages
Semantics
Formal Analysis
Notation

Language definitions as rewrite theories

Arusoaie, A., Lucanu, D., Rusu, V., Şerbǎnuţǎ, T. F., Ştefǎnescu, A. & Roşu, G., Jan 1 2014, In : Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 8663, p. 97-112 16 p.

Research output: Contribution to journalArticle

Maude
Computer programming languages
Semantics
Engines
Symbolic Execution

Maximal sound predictive race detection with control flow abstraction

Huang, J., O'Neil Meredith, P. & Rosu, G., Jun 5 2014, In : ACM SIGPLAN Notices. 49, 6, p. 337-348 12 p.

Research output: Contribution to journalArticle

Flow control
Acoustic waves
Detectors
Data storage equipment
Experiments

On the complexity of stream equality

Endrullis, J., Hendriks, D., Bakhshi, R. & Roşu, G., Jan 1 2014, In : Journal of Functional Programming. 24, 2-3, p. 166-217 52 p.

Research output: Contribution to journalArticle

Semantics

ROSRV: Runtime verification for robots

Huang, J., Erdogan, C., Zhang, Y., Moore, B., Luo, Q., Sundaresan, A. & Rosu, G., Jan 1 2014, In : Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 8734, p. 247-254 8 p.

Research output: Contribution to journalArticle

Runtime Verification
Robot
Robots
Reactive Oxygen Species
Monitor

The K primer (version 3.3)

Şerbǎnuţǎ, T. F., Arusoaie, A., Lazar, D., Ellison, C., Lucanu, D. & Rosu, G., Jun 10 2014, In : Electronic Notes in Theoretical Computer Science. 304, p. 57-80 24 p.

Research output: Contribution to journalArticle

Program Analysis
Computer programming languages
Programming Languages
Concurrent
State Space
2013

The rewriting logic semantics project: A progress report

Meseguer, J. & Roşu, G., Oct 10 2013, In : Information and Computation. 231, p. 38-69 32 p.

Research output: Contribution to journalArticle

Rewriting Logic
Semantics
Computer hardware
Scalability
Modeling Language
2012

An executable formal semantics of C with applications

Ellison, C. & Rosu, G., Jan 1 2012, In : ACM SIGPLAN Notices. 47, 1, p. 533-544 12 p.

Research output: Contribution to journalArticle

Semantics

An overview of the MOP runtime verification framework

Meredith, P. O. N., Jin, D., Griffith, D., Chen, F. & Roşu, G., Jun 1 2012, In : International Journal on Software Tools for Technology Transfer. 14, 3, p. 249-289 41 p.

Research output: Contribution to journalArticle

Monitoring
Specifications
Recovery

A rewriting logic approach to static checking of units of measurement in C

Hills, M., Chen, F. & Rosu, G., Dec 20 2012, In : Electronic Notes in Theoretical Computer Science. 290, p. 51-67 17 p.

Research output: Contribution to journalArticle

Rewriting Logic
Units of measurement
Unit
Static analysis
Annotation

Checking reachability using matching logic

Roşu, G. & Ştefǎnescu, A., Oct 1 2012, In : ACM SIGPLAN Notices. 47, 10, p. 555-574 20 p.

Research output: Contribution to journalArticle

Computer programming languages
Semantics

On safety properties and their monitoring

Roşu, G., Dec 5 2012, In : Scientific Annals of Computer Science. 22, 2, p. 327-365 39 p.

Research output: Contribution to journalArticle

Safety
Monitoring
Trace
Runtime Verification
Question Answering

Semantics and algorithms for parametric monitoring

Rosu, G. & Chen, F., Apr 26 2012, In : Logical Methods in Computer Science. 8, 1

Research output: Contribution to journalArticle

Trace analysis
Semantics
Trace
Monitoring
Slice
2010

An overview of the K semantic framework

Roşu, G. & Şerbǎnuţǎ, T. F., Aug 1 2010, In : Journal of Logic and Algebraic Programming. 79, 6, p. 397-434 38 p.

Research output: Contribution to journalArticle

Semantics
Calculus
Computer programming languages
Programming Languages
Term

Efficient monitoring of parametric context-free patterns

Meredith, P. O. N., Jin, D., Chen, F. & Roşu, G., Jun 1 2010, In : Automated Software Engineering. 17, 2, p. 149-180 32 p.

Research output: Contribution to journalArticle

Context free grammars
Monitoring
Temporal logic
Finite automata
Specifications
2009

A rewriting logic approach to operational semantics

Serbanuta, T. F., Rosu, G. & Meseguera, J., Feb 2009, In : Information and Computation. 207, 2, p. 305-340 36 p.

Research output: Contribution to journalArticle

Rewriting Logic
Operational Semantics
Semantics
Structural Operational Semantics
Abstract Machines

A semantic approach to interpolation

Popescu, A., Şerbǎnuţǎ, T. F. & Rosu, G., Mar 17 2009, In : Theoretical Computer Science. 410, 12-13, p. 1109-1128 20 p.

Research output: Contribution to journalArticle

Interpolation
Interpolate
Semantics
Algebraic Specification
Syntactics
2008

Regular Strategies as Proof Tactics for CIRC

Lucanu, D., Roşu, G. & Grigoraş, G., Apr 4 2008, In : Electronic Notes in Theoretical Computer Science. 204, C, p. 83-98 16 p.

Research output: Contribution to journalArticle

Rewriting
Engines
Coinduction
Maude
Regular Expressions
2007

A Rewrite Framework for Language Definitions and for Generation of Efficient Interpreters

Hills, M., Şerbǎnuţǎ, T. & Roşu, G., Jul 28 2007, In : Electronic Notes in Theoretical Computer Science. 176, 4, p. 215-231 17 p.

Research output: Contribution to journalArticle

Program interpreters
Computer programming languages
Rewriting Logic
Semantics
Specifications

A Rewriting Logic Approach to Operational Semantics (Extended Abstract)

Şerbǎnuţǎ, T. F., Rosu, G. & Meseguer, J., Oct 24 2007, In : Electronic Notes in Theoretical Computer Science. 192, 1 SPEC. ISS., p. 125-141 17 p.

Research output: Contribution to journalArticle

Rewriting Logic
Operational Semantics
Semantics
Structural Operational Semantics
One to one correspondence

MOP: An efficient and generic runtime verification framework

Chen, F. & Roşu, G., Oct 1 2007, In : ACM SIGPLAN Notices. 42, 10, p. 569-588 20 p.

Research output: Contribution to journalArticle

Specifications
Monitoring
Software engineering
Experiments
Defects

Rewriting Logic Systems

Denker, G., Talcott, C., Rosu, G., van den Brand, M., Eker, S. & Şerbǎnuţǎ, T. F., Jul 28 2007, In : Electronic Notes in Theoretical Computer Science. 176, 4, p. 233-247 15 p.

Research output: Contribution to journalArticle

Rewriting Logic
Rewriting

The rewriting logic semantics project

Meseguer, J. & Roşu, G., Apr 5 2007, In : Theoretical Computer Science. 373, 3, p. 213-237 25 p.

Research output: Contribution to journalArticle

Rewriting Logic
Semantics
Structural Operational Semantics
Algebraic Semantics
Maude
2006

Checking and Correcting Behaviors of Java Programs at Runtime with Java-MOP

Chen, F., d'Amorim, M. & Rosu, G., May 26 2006, In : Electronic Notes in Theoretical Computer Science. 144, 4 SPEC. ISS., p. 3-20 18 p.

Research output: Contribution to journalArticle

Computer programming
Java
Programming
Monitoring
Monitor

Equality of streams is a ∏ 2 0-complete problem

Roşu, G., Sep 1 2006, In : ACM SIGPLAN Notices. 41, 9, p. 184-191 8 p.

Research output: Contribution to journalArticle

Online efficient predictive safety analysis of multithreaded programs

Sen, K., Roşu, G. & Agha, G., Jun 1 2006, In : International Journal on Software Tools for Technology Transfer. 8, 3, p. 248-260 13 p.

Research output: Contribution to journalArticle

Specifications
Testing
Scalability
Clocks
Formal specification

The Rewriting Logic Semantics Project

Meseguer, J. & Roşu, G., May 15 2006, In : Electronic Notes in Theoretical Computer Science. 156, 1 SPEC. ISS., p. 27-56 30 p.

Research output: Contribution to journalArticle

Rewriting Logic
Semantics
Maude
Denotational Semantics
Program Analysis
2005

An equational specification for the Scheme language

D'Amorim, M. & Rosu, G., Sep 28 2005, In : Journal of Universal Computer Science. 11, 7, p. 1327-1348 22 p.

Research output: Contribution to journalArticle

Semantics
Specification
Specifications
Rewriting Systems
Equational Theory

Combining test case generation and runtime verification

Artho, C., Barringer, H., Goldberg, A., Havelund, K., Khurshid, S., Lowry, M., Pasareanu, C., Rosu, G., Sen, K., Visser, W. & Washington, R., May 18 2005, In : Theoretical Computer Science. 336, 2, p. 209-234 26 p.

Research output: Contribution to journalArticle

Runtime Verification
Temporal logic
Software testing
Temporal Logic
NASA

Monitoring Algorithms for Metric Temporal Logic Specifications

Thati, P. & Rosu, G., Jan 3 2005, In : Electronic Notes in Theoretical Computer Science. 113, SPEC. ISS., p. 145-162 18 p.

Research output: Contribution to journalArticle

Temporal logic
Temporal Logic
Monitoring
Specification
Specifications

Rewriting-based techniques for runtime verification

Rosu, G. & Havelund, K., Apr 1 2005, In : Automated Software Engineering. 12, 2, p. 151-197 47 p.

Research output: Contribution to journalArticle

Monitoring
Semantics
Temporal logic
Specification languages
Finite automata
2004
Software Development
Software engineering
Monitoring
Programming
Formal Specification

An Overview of the Runtime Verification Tool Java PathExplorer

Havelund, K. & Roşu, G., Mar 1 2004, In : Formal Methods in System Design. 24, 2, p. 189-215 27 p.

Research output: Contribution to journalArticle

Runtime Verification
Temporal logic
Java
Temporal Logic
Maude

Behavioral abstraction is hiding information

Roşu, G., Oct 25 2004, In : Theoretical Computer Science. 327, 1-2, p. 197-221 25 p.

Research output: Contribution to journalArticle

Information Hiding
Specifications
Theorem
Machinery
Algebraic Specification
Semantics
Module
Chemical analysis
Software
Technology

Efficient monitoring of safety properties

Havelund, K. & Roşu, G., Dec 1 2004, In : International Journal on Software Tools for Technology Transfer. 6, 2, p. 158-173 16 p.

Research output: Contribution to journalArticle

Temporal logic
Monitoring
Technical writing
NASA
Testing