Publications

2024

Haining Tong, Natalia Gavrilenko, Hernán Ponce de León, Keijo Heljanko: Towards Unified Analysis of GPU Consistency. ASPLOS [PDF]

Thomas Haas, René Maseli, Roland Meyer, Hernán Ponce de León: Static Analysis of Memory Models for SMT Encodings. OOPSLA [PDF]

Thomas Haas, Roland Meyer, Hernán Ponce de León: CAAT: Consistency as a Theory. OOPSLA [PDF]
Antonio Paolillo, Hernán Ponce de León, Thomas Haas, Diogo Behrens, Rafael Chehab, Ming Fu, Roland Meyer: Verifying and Optimizing Compact NUMA-Aware Locks on Weak Memory Models. Technical Report. [PDF]
Hernán Ponce de León, Johannes Kinder: Cats vs. Spectre: An Axiomatic Approach to Modeling Speculative Execution Attacks. S&P. [PDF]
Hernán Ponce de León, Thomas Haas, Roland Meyer: Dartagnan: SMT-based Violation Witness Validation (Competition Contribution). TACAS. [PDF]

Hernán Ponce de León, Thomas Haas, Roland Meyer: Dartagnan: Leveraging Compiler Optimizations and the Price of Precision (Competition Contribution). TACAS. [PDF]

Pierre Bouvier, Hubert Garavel, Hernán Ponce de León: Automatic Decomposition of Petri Nets into Automata Networks - A Synthetic Account. Petri Nets. [PDF]
Hernán Ponce de León, Florian Furbach, Keijo Heljanko, Roland Meyer: Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution). TACAS. [PDF]

Natalia Gavrilenko, Hernán Ponce de León, Florian Furbach, Keijo Heljanko, Roland Meyer: BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings. CAV. [PDF]

Hernán Ponce de León, Andrey Mokhov: Compact and efficiently verifiable models for concurrent systems. Formal Methods Syst. Des.[PDF]
Hernán Ponce de León, Lucio Nardelli, Josep Carmona, Seppe K. L. M. vanden Broucke: Incorporating negative information to process discovery of complex systems. Inf. Sci. [PDF]
Hernán Ponce de León, Florian Furbach, Keijo Heljanko, Roland Meyer: BMC with Memory Models as Modules. FMCAD. [PDF]

Olli Saarikivi, Hernán Ponce de León, Kari Kähkönen, Keijo Heljanko, Javier Esparza: Minimizing Test Suites with Unfoldings of Multithreaded Programs. ACM Trans. Embed. Comput. Syst. [PDF]
Hernán Ponce de León, Florian Furbach, Keijo Heljanko, Roland Meyer: Portability Analysis for Weak Memory Models. PORTHOS: One Tool for all Models. SAS. [PDF]
Hernán Ponce de León, Stefan Haar, Delphine Longuet: Model-based testing for concurrent systems: unfolding-based test selection. Int. J. Softw. Tools Technol. Transf. [PDF]

Hernán Ponce de León, Olli Saarikivi, Kari Kähkönen, Keijo Heljanko, Javier Esparza: Unfolding Based Minimal Test Suites for Testing Multithreaded Programs. ACSD. [PDF]

Hernán Ponce de León, César Rodríguez, Josep Carmona, Keijo Heljanko, Stefan Haar: Unfolding-Based Process Discovery. ATVA. [PDF]
Hernán Ponce de León, César Rodríguez, Josep Carmona: POD - A Tool For Process Discovery Using Partial Orders and Independence Information. BPM (Demos). [PDF]
Hernán Ponce de León, Josep Carmona, Seppe K. L. M. vanden Broucke: Incorporating Negative Information in Process Discovery. BPM. [PDF]
Hernán Ponce de León, Andrey Mokhov: Building Bridges Between Sets of Partial Orders. LATA. [PDF]
Konstantinos Athanasiou, Hernán Ponce de León, Stefan Schwoon: Test Case Generation for Concurrent Systems Using Event Structures. TAP@STAF. [PDF]

Hernán Ponce de León, Stefan Haar, Delphine Longuet: Model-based testing for concurrent systems with labelled event structures. Softw. Test. Verification Reliab.
Hernán Ponce de León, Stefan Haar, Delphine Longuet: Distributed Testing of Concurrent Systems: Vector Clocks to the Rescue. ICTAC.

Hernán Ponce de León, Stefan Haar, Delphine Longuet: Unfolding-Based Test Selection for Concurrent Conformance. ICTSS.

Hernán Ponce de León, Stefan Haar, Delphine Longuet: Conformance Relations for Labeled Event Structures. TAP@TOOLS.