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

Search results

  • 2021

    Language-parametric compiler validation with application to LLVM

    Kasampalis, T., Park, D., Lin, Z., Adve, V. S. & Rosu, G., Apr 19 2021, Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2021. Association for Computing Machinery, p. 1004-1019 16 p. (International Conference on Architectural Support for Programming Languages and Operating Systems - ASPLOS).

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

  • Matching logic explained

    Chen, X., Lucanu, D. & Roşu, G., Apr 2021, In: Journal of Logical and Algebraic Methods in Programming. 120, 100638.

    Research output: Contribution to journalArticlepeer-review

  • The K Vision for the Future of Programming Language Design and Analysis

    Chen, X. & Roşu, G., 2021, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer, p. 3-9 7 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 13065 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingChapter

  • Towards a Trustworthy Semantics-Based Language Framework via Proof Generation

    Chen, X., Lin, Z., Trinh, M. T. & Roşu, G., 2021, Computer Aided Verification - 33rd International Conference, CAV 2021, Proceedings. Silva, A. & Leino, K. R. (eds.). Springer, p. 477-499 23 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12760 LNCS).

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

    Open Access
  • 2020

    A general approach to define binders using matching logic

    Chen, X. & Rosu, G., Aug 2 2020, In: Proceedings of the ACM on Programming Languages. 4, ICFP, 88.

    Research output: Contribution to journalArticlepeer-review

    Open Access
  • Connecting Constrained Constructor Patterns and Matching Logic

    Chen, X., Lucanu, D. & Roşu, G., 2020, Rewriting Logic and Its Applications - 13th International Workshop, WRLA 2020, Revised Selected Papers. Escobar, S. & Martí-Oliet, N. (eds.). Springer, p. 19-37 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12328 LNCS).

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

  • End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract

    Park, D., Zhang, Y. & Rosu, G., 2020, Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings. Lahiri, S. K. & Wang, C. (eds.). Springer, p. 151-164 14 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12224 LNCS).

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

    Open Access
  • Formalizing Correct-by-Construction Casper in Coq

    Li, E., Serbanuta, T., Diaconescu, D., Zamfir, V. & Rosu, G., May 2020, IEEE International Conference on Blockchain and Cryptocurrency, ICBC 2020. Institute of Electrical and Electronics Engineers Inc., 9169468. (IEEE International Conference on Blockchain and Cryptocurrency, ICBC 2020).

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

  • K—A semantic framework for programming languages and formal analysis

    Chen, X. & Roşu, G., 2020, Engineering Trustworthy Software Systems - 5th International School, SETSS 2019, Tutorial Lectures. Bowen, J. P., Liu, Z. & Zhang, Z. (eds.). Springer, p. 122-158 37 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12154 LNCS).

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

  • Message from the ICBC2020 General and Technical Program Chairs

    Plataniotis, K., Veneris, A., Kanhere, S., Rosu, G. & William, K., May 2020, In: IEEE International Conference on Blockchain and Cryptocurrency, ICBC 2020. 9169461.

    Research output: Contribution to journalEditorialpeer-review

    Open Access
  • Message from the ICBC2020 General and Technical Program Chairs

    Plataniotis, K., Veneris, A., Kanhere, S., Rosu, G. & William, K., May 2020, In: IEEE International Conference on Blockchain and Cryptocurrency, ICBC 2020. p. 5-6 2 p., 9169409.

    Research output: Contribution to journalEditorialpeer-review

    Open Access
  • Statistical model checking of randao’s resilience to pre-computed reveal strategies

    Alturki, M. A. & Roşu, G., 2020, Formal Methods- FM 2019 International Workshops - Revised Selected Papers. Sekerinski, E., Moreira, N., Oliveira, J. N., Ratiu, D., Guidotti, R., Farrell, M., Luckcuck, M., Marmsoler, D., Campos, J., Astarte, T., Gonnord, L., Cerone, A., Couto, L., Dongol, B., Kutrib, M., Monteiro, P. & Delmas, D. (eds.). Springer, p. 337-349 13 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12232 LNCS).

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

  • Towards a unified proof framework for automated fixpoint reasoning using matching logic

    Chen, X., Trinh, M. T., Rodrigues, N., Peña, L. & Roşu, G., Nov 13 2020, In: Proceedings of the ACM on Programming Languages. 4, OOPSLA, 161.

    Research output: Contribution to journalArticlepeer-review

    Open Access
  • Towards a verified model of the algorand consensus protocol in coq

    Alturki, M. A., Chen, J., Luchangco, V., Moore, B., Palmskog, K., Peña, L. & Roşu, G., 2020, Formal Methods- FM 2019 International Workshops - Revised Selected Papers. Sekerinski, E., Moreira, N., Oliveira, J. N., Ratiu, D., Guidotti, R., Farrell, M., Luckcuck, M., Marmsoler, D., Campos, J., Astarte, T., Gonnord, L., Cerone, A., Couto, L., Dongol, B., Kutrib, M., Monteiro, P. & Delmas, D. (eds.). Springer, p. 362-367 6 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12232 LNCS).

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

  • 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
  • All-Path reachability logic

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

    Research output: Contribution to journalArticlepeer-review

  • 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 journalArticlepeer-review

  • 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 journalArticlepeer-review

    Open Access
  • 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 journalArticlepeer-review

  • 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., 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

  • 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

  • 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

  • Runtime verification-17 years later

    Havelund, K. & Roşu, G., 2019, Runtime Verification- 18th International Conference, RV 2018, Proceedings. Colombo, C. & Leucker, M. (eds.). Springer, 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 past experiences and future projections

    Havelund, K., Reger, G. & Roşu, G., 2019, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer, p. 532-562 31 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10000).

    Research output: Chapter in Book/Report/Conference proceedingChapter

    Open Access
  • 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

  • 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

  • A language-independent approach to smart contract verification

    Chen, X., Park, D. & Roşu, G., 2018, Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice - 8th International Symposium, ISoLA 2018, Proceedings. Margaria, T. & Steffen, B. (eds.). Springer, 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

  • A language-independent program verification framework

    Chen, X. & Roşu, G., 2018, Leveraging Applications of Formal Methods, Verification and Validation. Verification - 8th International Symposium, ISoLA 2018, Proceedings. Margaria, T. & Steffen, B. (eds.). Springer, 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

  • Finite-trace linear temporal logic: coinductive completeness

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

    Research output: Contribution to journalArticlepeer-review

  • 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. Kirchner, H. (ed.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 108).

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

  • 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

  • Program verification by coinduction

    Moore, B., Peña, L. & Rosu, G., 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, 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

  • 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

  • Matching logic

    Roşu, G., 2017, In: Logical Methods in Computer Science. 13, 4, 28.

    Research output: Contribution to journalArticlepeer-review

  • Maximizing concurrency bug detection in multithreaded software programs

    Huang, J. & Rosu, G., Oct 17 2017, U.S. Patent No. 9792161, Nov 25 2014

    Research output: Patent

  • 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 journalArticlepeer-review

  • Finite-trace linear temporal logic: Coinductive completeness

    Roşu, G., 2016, Runtime Verification - 16th International Conference, RV 2016, Proceedings. Falcone, Y. & Sánchez, C. (eds.). Springer, 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

  • 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

  • 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 journalArticlepeer-review

    Open Access
  • 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, (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

  • 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, 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

  • RV-ECU: Maximum Assurance In-Vehicle Safety Monitoring

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

    Research output: Contribution to journalConference articlepeer-review

  • RV-match: Practical semantics-based program analysis

    Guth, D., Hathhorn, C., Saxena, M. & Roşu, G., 2016, Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings. Farzan, A. & Chaudhuri, S. (eds.). Springer, 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

  • Semantics-based program verifiers for all languages

    Stefanescu, A., Park, D., Yuwen, S., Li, Y. & Roşu, G., Oct 19 2016, In: ACM SIGPLAN Notices. 51, 10, p. 74-91 18 p.

    Research output: Contribution to journalArticlepeer-review

    Open Access
  • 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

    Open Access
  • 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, 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

  • 2015

    A theoretical foundation for programming languages aggregation

    Ciobâcă, Ş., Lucanu, D., Rusu, V. & Roşu, G., 2015, Recent Trends in Algebraic Development Techniques - 22nd International Workshop, WADT 2014, Revised Selected Papers. Ţuţu, I., Codescu, M. & Diaconescu, R. (eds.). Springer, 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

  • 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

  • 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 journalArticlepeer-review

  • 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