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

Research Output 1997 2019

2019

A complete formal semantics of x86-64 user-level instruction set architecture

Dasgupta, S., Park, D., Kasampalis, T., Adve, V. S. & Roşu, G., Jun 8 2019, PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. McKinley, K. S. & Fisher, K. (eds.). Association for Computing Machinery, p. 1133-1148 16 p. (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Open Access
Semantics
Testing

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

IELE: A rigorously designed language and tool ecosystem for the blockchain

Kasampalis, T., Guth, D., Moore, B., Șerbănuță, T. F., Zhang, Y., Filaretti, D., Șerbănuță, V., Johnson, R. & Roşu, G., Jan 1 2019, Formal Methods – The Next 30 Years - 3rd World Congress, FM 2019, Proceedings. ter Beek, M. H., McIver, A. & Oliveira, J. N. (eds.). Springer, p. 593-610 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11800 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Ecosystem
Ecosystems
Formal Verification
Virtual Machine
High level languages

Matching µ-logic: Foundation of K framework

Chen, X. & Roşu, G., Nov 2019, 8th Conference on Algebra and Coalgebra in Computer Science, CALCO 2019. Roggenbach, M. & Sokolova, A. (eds.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 1. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 139).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Semantics
Temporal logic
Computer programming languages
Costs

Matching μ-Logic

Chen, X. & Rosu, G., Jun 2019, 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019. Institute of Electrical and Electronics Engineers Inc., 8785675. (Proceedings - Symposium on Logic in Computer Science; vol. 2019-June).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Temporal logic
Computer programming languages
Acoustic waves
Logic
Pattern matching

Runtime verification-17 years later

Havelund, K. & Roşu, G., Jan 1 2019, Runtime Verification- 18th International Conference, RV 2018, Proceedings. Colombo, C. & Leucker, M. (eds.). Springer-Verlag, p. 3-17 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11237).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Runtime Verification
Trace
Specifications
Runtime Analysis
Specification

Techniques for evolution-aware runtime verification

Legunsen, O., Zhang, Y., Hadzi-Tanovic, M., Rosu, G. & Marinov, D., Apr 2019, Proceedings - 2019 IEEE 12th International Conference on Software Testing, Verification and Validation, ICST 2019. Institute of Electrical and Electronics Engineers Inc., p. 300-311 12 p. 8730172. (Proceedings - 2019 IEEE 12th International Conference on Software Testing, Verification and Validation, ICST 2019).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Monitoring
Feedback
2018

A formal verification tool for ethereum VM bytecode

Park, D., Zhang, Y., Saxena, M., Daian, P. & Roşu, G., Oct 26 2018, ESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European So ftware Engineering Conference and Symposium on the Foundations of So ftware Engineering. Garci, A., Pasareanu, C. S. & Leavens, G. T. (eds.). Association for Computing Machinery, Inc, p. 912-915 4 p. (ESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Virtual machine
Formal verification
Scalability
Semantics

A language-independent approach to smart contract verification

Chen, X., Park, D. & Roşu, G., Jan 1 2018, Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice - 8th International Symposium, ISoLA 2018, Proceedings. Margaria, T. & Steffen, B. (eds.). Springer-Verlag, p. 405-413 9 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11247 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Language
Framework
Style

A language-independent program verification framework

Chen, X. & Roşu, G., Jan 1 2018, Leveraging Applications of Formal Methods, Verification and Validation. Verification - 8th International Symposium, ISoLA 2018, Proceedings. Margaria, T. & Steffen, B. (eds.). Springer-Verlag, p. 92-102 11 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11245 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Program Verification
Semantics
Operational Semantics
Framework
Language

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

Formal design, implementation and verification of blockchain languages

Rosu, G., Jul 1 2018, 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, Vol. 108. 2

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Semantics
Virtual machine

KEVM: A complete formal semantics of the ethereum virtual machine

Hildenbrandt, E., Saxena, M., Rodrigues, N., Zhu, X., Daian, P., Guth, D., Moore, B., Park, D., Zhang, Y., Stefanescu, A. & Rosu, G., Aug 7 2018, Proceedings - IEEE 31st Computer Security Foundations Symposium, CSF 2018. IEEE Computer Society, p. 204-217 14 p. 8429306. (Proceedings - IEEE Computer Security Foundations Symposium; vol. 2018-July).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Semantics
Specifications
Formal methods
Cryptography
Virtual machine

Program verification by coinduction

Moore, B., Peña, L. & Rosu, G., Jan 1 2018, Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings. Ahmed, A. (ed.). Springer-Verlag, p. 589-618 30 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10801 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Coinduction
Program Verification
Semantics
Automation
Operational Semantics
2017

K: A semantic framework for programming languages and formal analysis tools

Rosu, G., Jan 1 2017, Dependable Software Systems Engineering. IOS Press, p. 186-206 21 p.

Research output: Chapter in Book/Report/Conference proceedingChapter

Computer programming languages
Semantics

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

Finite-trace linear temporal logic: Coinductive completeness

Roşu, G., Jan 1 2016, Runtime Verification - 16th International Conference, RV 2016, Proceedings. Falcone, Y. & Sánchez, C. (eds.). Springer-Verlag, p. 333-350 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10012 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Linear Temporal Logic
Temporal logic
Completeness
Trace
Runtime Verification

How good are the specs? A study of the bug-finding effectiveness of existing Java api specifications

Legunsen, O., Ul Hassan, W., Xu, X., Roşu, G. & Marinov, D., Aug 25 2016, ASE 2016 - Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering. Khurshid, S., Lo, D. & Apel, S. (eds.). Association for Computing Machinery, Inc, p. 602-613 12 p. (ASE 2016 - Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Specifications
Application programming interfaces (API)
Software engineering
Monitoring
Testing

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

Program verification using reachability logic

Roşu, G., Ştefănescu, A. & Ciobâcă, Ş., Jan 1 2016, Rewriting Logic and Its Applications - 11th International Workshop, WRLA 2016 Held as a Satellite Event of ETAPS 2016, Revised Selected Papers. Lucanu, D. (ed.). Springer-Verlag, (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9942 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Program Verification
Reachability
Semantics
Logic
Equivalence

Runtime verification at work: A tutorial

Daian, P., Guth, D., Hathhorn, C., Li, Y., Pek, E., Saxena, M., Şerbănuţă, T. F. & Roşu, G., Jan 1 2016, Runtime Verification - 16th International Conference, RV 2016, Proceedings. Falcone, Y. & Sánchez, C. (eds.). Springer-Verlag, p. 46-67 22 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10012 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Runtime Verification
Monitor
Detector
Acoustic waves
Detectors

RV-ECU: Maximum Assurance In-Vehicle Safety Monitoring

Daian, P., Shiraishi, S., Iwai, A., Manja, B. & Rosu, G., Jan 1 2016, In : SAE Technical Papers.

Research output: Contribution to journalConference article

Monitoring
Specifications
Railroad cars
Communication
Costs

RV-match: Practical semantics-based program analysis

Guth, D., Hathhorn, C., Saxena, M. & Roşu, G., Jan 1 2016, Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings. Farzan, A. & Chaudhuri, S. (eds.). Springer-Verlag, p. 447-453 7 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9779).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Program Analysis
Semantics
Formal Semantics
Beat
Correctness

Semantics-based program verifiers for all languages

Stefánescu, A., Park, D., Yuwen, S., Li, Y. & Rosu, G., Oct 19 2016, OOPSLA 2016 - Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications. Visser, E. & Smaragdakis, Y. (eds.). Association for Computing Machinery, p. 74-91 18 p. (Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA; vol. 02-04-November-2016).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Semantics
Specifications
Data structures
Acoustic waves

Towards a Kool Future

Lucanu, D., Şerbănuţă, T. F. & Rosu, G., Jan 1 2016, Theory and Practice of Formal Methods - Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday. Ábrahám, E., Bonsangue, M. & Johnsen, E. B. (eds.). Springer-Verlag, p. 325-343 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9660).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Object oriented programming
Semantics
JavaScript
Object-oriented Programming
Formal Semantics
2015

A theoretical foundation for programming languages aggregation

Ciobâcă, Ş., Lucanu, D., Rusu, V. & Roşu, G., Jan 1 2015, Recent Trends in Algebraic Development Techniques - 22nd International Workshop, WADT 2014, Revised Selected Papers. Ţuţu, I., Codescu, M. & Diaconescu, R. (eds.). Springer-Verlag, p. 30-47 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9463).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Computer programming languages
Programming Languages
Aggregation
Agglomeration
Semantics

Defining the undefinedness of C

Hathhorn, C., Ellison, C. & Roşu, G., Jun 3 2015, PLDI 2015 - Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation. Blackburn, S. & Grove, D. (eds.). Association for Computing Machinery, p. 336-345 10 p. (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI); vol. 2015-June).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Semantics

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

Evolution-Aware Monitoring-Oriented Programming

Legunsen, O., Marinov, D. & Rosu, G., Aug 12 2015, Proceedings - 2015 IEEE/ACM 37th IEEE International Conference on Software Engineering, ICSE 2015. IEEE Computer Society, p. 615-618 4 p. 7203026. (Proceedings - International Conference on Software Engineering; vol. 2).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Monitoring
Experiments

From rewriting logic, to programming language semantics, to program verification

Roşu, G., Jan 1 2015, Logic, Rewriting and Concurrency - Essays Dedicated to Jose Meseguer on the Occasion of His 65th Birthday. Ölveczky, P. C., Talcott, C. & Martí-Oliet, N. (eds.). Springer-Verlag, p. 598-616 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9200).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Rewriting Logic
Program Verification
Computer programming languages
Programming Languages
Semantics

GPredict: Generic predictive concurrency analysis

Huang, J., Luo, Q. & Rosu, G., Aug 12 2015, Proceedings - 2015 IEEE/ACM 37th IEEE International Conference on Software Engineering, ICSE 2015. IEEE Computer Society, p. 847-857 11 p. 7194631. (Proceedings - International Conference on Software Engineering; vol. 1).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Trace analysis
Surface mount technology

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

K-Java: A complete semantics of Java

Bogdənaş, D. & Rosu, G., Jan 14 2015, POPL 2015 - Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Association for Computing Machinery, p. 445-456 12 p. (Conference Record of the Annual ACM Symposium on Principles of Programming Languages; vol. 2015-January).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Semantics

KJS: A complete formal semantics of JavaScript

Park, D., Ştefənescu, A. & Roşu, G., Jun 3 2015, PLDI 2015 - Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation. Blackburn, S. & Grove, D. (eds.). Association for Computing Machinery, p. 346-356 11 p. (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI); vol. 2015-June).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Semantics
Acceptance tests
Engines

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

Matching logic - extended abstract

Rosu, G., Jun 1 2015, 26th International Conference on Rewriting Techniques and Applications, RTA 2015. Fernandez, M. (ed.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, p. 5-21 17 p. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 36).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Pattern matching
Acoustic waves
Surface mount technology
Computer programming languages
Semantics

RV-android: Efficient parametric android runtime verification, a brief tutorial

Daian, P., Falcone, Y., Meredith, P., Şerbǎnuţǎ, T. F., Shiriashi, SI., Akihito, A. I. & Rosu, G., Jan 1 2015, Runtime Verification - 6th International Conference, RV 2015, Proceedings. Bartocci, E. & Majumdar, R. (eds.). Springer-Verlag, p. 342-357 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9333).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Runtime Verification
Monitoring
Monitor
Safety
Expressiveness

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

A language-independent proof system for mutual program equivalence

Ciobâcă, Ş., Lucanu, D., Rusu, V. & Roşu, G., Jan 1 2014, Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, ICFEM 2014, Proceedings. Merz, S. & Pang, J. (eds.). Springer-Verlag, p. 75-90 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8829).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Proof System
Semantics
Equivalence
Operational Semantics
Terminate

All-path reachability logic

Ştefǎnescu, A., Ciobâč, Ş., Mereuta, R., Moore, B. M., Şerbǎnutǎ, T. F. & Rosu, G., Jan 1 2014, Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Springer-Verlag, p. 425-440 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8560 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Reachability
Proof System
Semantics
Logic
Path
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

Maximal sound predictive race detection with control flow abstraction

Huang, J., Meredith, P. O. N. & Rosu, G., Jan 1 2014, PLDI 2014 - Proceedings of the 2014 ACM SIGPLAN Conference on Programming Language Design and Implementation. Association for Computing Machinery, p. 337-348 12 p. (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Flow control
Acoustic waves
Detectors
Data storage equipment
Experiments