Document Open Access Logo

Debugging a Smalltalk VM Assisted by Large Automated Reasoning (Extended Abstract)

Authors Boris Shingarov , Jan Vraný

PDF HTML 5

Files

Thumbnail PDF
PDF
OASIcs.Programming.2025.4.pdf
  • Filesize: 0.49 MB
  • 6 pages
HTML5 Logo HTML (experimental)
OASIcs.Programming.2025.4.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → Semantics
  • Software and its engineering → Runtime environments
  • Theory of computation → Operational semantics
Keywords
  • Smalltalk
  • Virtual Machine
  • Automated Reasoning
  • Debugging
  • ISA Specification

Metrics

Abstract

We show how a full-scale automated-reasoning engine implemented in Smalltalk can be applied to assist in the programmer’s cognitive task of traversing abstraction levels. This approach follows naturally from our definition of debugging as any activity aimed towards understanding a program. We introduce the notion of "dimensions of abstraction", give two examples ("stratum" and "mode"), and show how it is applied in debugging a native compiler backend.

Cite As Get BibTex

Boris Shingarov and Jan Vraný. Debugging a Smalltalk VM Assisted by Large Automated Reasoning (Extended Abstract). In Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming (Programming 2025). Open Access Series in Informatics (OASIcs), Volume 134, pp. 4:1-4:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/OASIcs.Programming.2025.4

Author Details

Boris Shingarov
  • LabWare, Monkton, Canada
Jan Vraný
  • LabWare, Dundee, UK

References

  1. Jade Alglave, Patrick Cousot, and Luc Maranget. Syntax and semantics of the weak consistency model specification language cat. CoRR, abs/1608.07531, 2016. URL: https://doi.org/10.48550/arXiv.1608.07531.
  2. Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell. ISA semantics for ARMv8-A, RISC-V, and CHERI-MIPS. In Proc. 46th ACM SIGPLAN Symposium on Principles of Programming Languages, volume 3, pages 71:1-71:31, 2019. Proc. ACM Program. Lang. 3, POPL, Article 71. URL: https://doi.org/10.1145/3290384.
  3. Gilad Bracha and Arthur Ryman. JSR 45: Debugging Support for Other Languages. URL: https://jcp.org/en/jsr/detail?id=45.
  4. Andrei Chis, Tudor Gîrba, and Oscar Nierstrasz. The moldable debugger: A framework for developing domain-specific debuggers. In Benoît Combemale, David J. Pearce, Olivier Barais, and Jurgen J. Vinju, editors, Software Language Engineering - 7th International Conference, SLE 2014, Västerås, Sweden, September 15-16, 2014. Proceedings, volume 8706 of Lecture Notes in Computer Science, pages 102-121. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-11245-9_6.
  5. Leonardo Mendonça de Moura and Nikolaj S. Bjørner. Z3: an efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science, pages 337-340, Berlin, Heidelberg, 2008. Springer. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  6. Daniel Ingalls, Eliot Miranda, Clément Béra, and Elisa Gonzalez Boix. Two decades of live coding and debugging of virtual machines through simulation. Softw. Pract. Exp., 50(9):1629-1650, 2020. URL: https://doi.org/10.1002/SPE.2841.
  7. Java Platform Debugger Architecture (JPDA). URL: https://docs.oracle.com/javase/8/docs/technotes/guides/jpda/.
  8. Boris Shingarov. What is "debugging" anyway? Experiences with target-agnostic Cog, 2020. URL: https://www.youtube.com/watch?v=kFni50djp9k.
  9. Boris Shingarov and Jan Vraný. Towards a Dynabook for verified VM construction. J. Comput. Lang., 80:101275, 2024. URL: https://doi.org/10.1016/J.COLA.2024.101275.
  10. Boris G Shingarov. Live proof-by-induction. In FAST Workshop 2022 on Smalltalk Related Technologies, 2022. URL: https://openreview.net/forum?id=AaMvINlc7d.
  11. Yan Shoshitaishvili, Ruoyu Wang, Christopher Salls, Nick Stephens, Mario Polino, Andrew Dutcher, John Grosen, Siji Feng, Christophe Hauser, Christopher Krügel, and Giovanni Vigna. SOK: (state of) the art of war: Offensive techniques in binary analysis. In IEEE Symposium on Security and Privacy, SP 2016, San Jose, CA, USA, May 22-26, 2016, pages 138-157. IEEE Computer Society, 2016. URL: https://doi.org/10.1109/SP.2016.17.
  12. Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala. Refinement Reflection: Complete Verification with SMT. Proc. ACM Program. Lang., 2(POPL), December 2017. URL: https://doi.org/10.1145/3158141.
  13. Jan Vraný and Boris Shingarov. Tinyrossa: A compiler framework for vertical, verified construction of Smalltalk VMs. In Emma Söderberg and Luke Church, editors, Companion Proceedings of the 8th International Conference on the Art, Science, and Engineering of Programming, Programming Companion 2024, Lund, Sweden, March 11-15, 2024. ACM, 2024. URL: https://doi.org/10.1145/3660829.3660838.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact