A5006995825- Parallel Computing and Optimization Techniques
- Superconducting Materials and Applications
- Security and Verification in Computing
- Logic, programming, and type systems
- Formal Methods in Verification
- Embedded Systems Design Techniques
- Radiation Effects in Electronics
- Advanced Software Engineering Methodologies
- Simulation Techniques and Applications
- Advanced Malware Detection Techniques
- Advanced Data Storage Technologies
- Service-Oriented Architecture and Web Services
- Distributed systems and fault tolerance
Acceleware (Canada)
2024
The open-source and community-supported gem5 simulator is one of the most popular tools for computer architecture research. This simulation infrastructure allows researchers to model modern hardware at cycle level, it has enough fidelity boot unmodified Linux-based operating systems run full applications multiple architectures including x86, Arm, RISC-V. been under active development over last nine years since original release. In this time, there have 7500 commits codebase from 250 unique...
A debugging system is described wherein an outer Smalltalk running on a real machine interacts with GEM5 simulation of inner Smalltalk. An experimental embodiment applied towards understanding the behavior target-agnostic JIT prototype.
We present Smalltalk-25, a scientific Programm of research towards the synthesis Smalltalk VMs by formal methods. approach this through Dynabook-style implementation Hilbert's "manipulating proofs as mathematical objects". begin implementing an automated-reasoning engine based on refinement types. Having that foundation laid, we build program logics for simple "model" language; framework reasoning about real intermediate language translating into model ahead-of-time bootstrapper; and...
We describe an experimental attempt at verification of Smalltalk VM using mechanized proof. Only the native code generation part is verified. The generator developed in Coq proof assistant and largely based on CompCert compiler backend. resulting successfully runs ANSI test suite a number targets with different ISAs.