Institute of

Theoretical Computer Science

Carl-Friedrich-Gauß-Fakultät

Technische Universität Braunschweig

Emanuele D'Osualdo, PhD

emanuele.dosualdo

My research interests include Semantics, Models of Concurrency, Static Analysis, Process Algebra, Abstract Interpretation, Model Checking, Programming Languages, and Declarative Programming.

Personal website Full CV

Short Bio

2017–current	Research Associate at Imperial College London, UK.
2015–2017	PostDoc at the Concurrency Theory Group, TU Kaiserslautern, Germany. Working with Roland Meyer.
2015	PhD in Computer Science, University of Oxford, UK. Supervisor: Prof. C.-H. Luke Ong. My PhD thesis won the BCS/CHPC Distinguished Dissertation Award.
2010	MSc in Computer Science, University of Udine, Italy. Graduated with honors.

Teaching @ Uni-KL

Concurrency Theory (WS'16/17)
Advanced Automata Theory (SS'16)

News

LICS 2024: On the Separability Problem of VASS Reachability Languages has been accepted. publications
ICALP 2024: Separability in Büchi Vass and Singly Non-Linear Systems of Inequalities has been accepted. publications
SV-COMP 2024 Gold Medals: Dartagnan won two gold medals at SV-COMP2024. It won both as verifier and validator in the ConcurrencySafety category.
CONCUR 2023 Best Paper Award: For Separability and non-determinizability of WSTS. publications
OOPSLA 2023: Static Analysis of Memory Models for SMT Encodings has been accepted. publications
CONCUR 2023: Separability and non-determinizability of WSTS has been accepted. publications
Dr. rer. nat. Sebastian Muskalla: Congratulations on your successful defense!
CAV 2023: nekton: a linearizability proof checker has been accepted. publications
Andrzej Murawski @ TU-BS: Congratulations to Andrzej on winning a Humboldt Research Award. Andrzej will spend a sabbatical at TU Braunschweig.
PLDI 2023: Embedding Hindsight Reasoning in Separation Logic has been accepted. publications
TACAS 2023: Make flows small again: revisiting the flow framework has been accepted. publications
OOPSLA 2022 Distinguished Paper Award: For CAAT: Consistency as a Theory. publications
STACS 2023: Regular Separability in Büchi Vector Addition Systems has been accepted. publications
APLAS 2022: Model-based Fault Classification for Automotive Software has been accepted. publications
OOPSLA 2022: CAAT: Consistency as a Theory has been accepted. publications
OOPSLA 2022: A Concurrent Program Logic with a Future and History has been accepted. publications
Dr. rer. nat. Peter Chini: Congratulations on your successful defense!
PODC 2022: Parameterized Verification under Release Acquire is PSPACE-complete has been accepted. publications
ETAPS Best Dissertation Award: Congratulations Sebastian on winning the 2022 ETAPS Doctoral Dissertation Award. Sebastian's thesis “Verifying Non-blocking Data Structures with Manual Memory Management” can be found here
TACAS 2022 (SVCOMP): Dartagnan: SMT-based Violation Witness Validation has been accepted. publications
Journal of Computing: Liveness in Broadcast Networks has been accepted. publications
Dr. rer. nat. Sebastian Wolff: Congratulations on your successful defense!
NETYS 2021: Petri Net Invariant Synthesis has been accepted. publications
Simons Junior Fellow: Sebastian Wolff will join the Simons Society of Fellows and move to NYU. Congratulations!
IAV: Joint project Virtual Test Analyzer 3 with IAV. research
TACAS 2021: Dartagnan: Leveraging Compiler Optimizations and the Price of Precision has been accepted. publications
Dr.-Ing. Florian Furbach: Congratulations on your successful defense!
FSTTCS 2020: A Framework for Consistency Algorithms has been accepted. publications
FSTTCS 2020: On the Complexity of Multi-Pushdown Games has been accepted. publications
CAV 2020: Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games has been accepted. publications
NETYS 2020: Safety Verification under Power has been accepted. publications
Journal of Automated Reasoning: Fine-Grained Complexity of Safety Verification has been accepted. publications
TACAS 2020: Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution). publications
IAV: Joint project Virtual Test Analyzer 2 with ISF and IAV. research
POPL 2020: Pointer Life Cycle Types for Lock-Free Data Structures with Memory Reclamation has been accepted. publications
FSTTCS 2019: Complexity of Liveness in Parameterized Systems has been accepted. publications
Best student paper @ NETYS 2019: Congratulations to Peter on winning the award for his paper Liveness in Broadcast Networks. publications
Parameterized Complexity Newsletter: Fine-Grained Complexity of Program Verification Tasks. publications
CAV 2019: BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings has been accepted. publications
DAAD: Our project Functional Reactive Program Verification has been granted. research
Prakash Saivasan @ IMSc: Congratulations to Prakash for his assistant professor position at IMSc.
DAC 2019: Temporal Tracing of On-chip Signals using Timeprints has been accepted. publications
Ahmed Bouajjani @ TU-BS: Congratulations to Ahmed on winning a Humboldt Research Award. Ahmed will spend a month at TU Braunschweig.
DFG: Our project EDS @ SYN: Effective Denotational Semantics for Synthesis has been granted. research
IAV: Joint project Virtual Test Analyzer with ISF and IAV. research
Georg Zetzsche @ MPI-SWS: Congratulations to Georg for his position at MPI-SWS. His team is called Models of Computation.
POPL 2019: Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis has been accepted. publications
IFIP WG 2.2: Roland Meyer has been elected as a member of the IFIP Working Group 2.2 Formal Description of Programming Concepts.
FMCAD 2018: BMC with Memory Models as Modules. publications
MFCS 2018: Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems. publications
CONCUR 2018: Regular Separability of Well-Structured Transition Systems. publications
CONCUR 2018: Verifying Quantitative Temporal Properties of Procedural Programs. publications
CONCUR 2018: Bounded Context Switching for Valence Systems. publications
TACAS 2018: Fine-Grained Complexity of Safety Verification. publications
FSTTCS 2017: Verification of Asynchronous Programs with Nested Locks. publications
SEP Award 2017: Congratulations to the UnicornPL project teams on winning the SEP award 2017!
ESA 2017: On the Complexity of Bounded Context Switching. publications
MFCS 2017: Domains for Higher-Order Games. publications
MFCS 2017: On the Upward/Downward Closures of Petri Nets. publications
SAS 2017: Effect Summaries for Thread-Modular Analysis. publications
SAS 2017: Portability Analysis for Weak Memory Models. Porthos: One Tool for all Models. publications
GI-Fachgruppe: Roland Meyer has been elected as the spokesperson of the GI-Fachgruppe Concurrency Theory.
NETYS 2017: Locality and Singularity for Store-Atomic Memory Models. publications
Dr.-Ing. Georgel Calin: Congratulations on your successful defense!
BCS/CHPC Distinguished Dissertation Award: The thesis “Verification of Message Passing Concurrent Systems” (by Emanuele D'Osualdo) received the BCS/CHPC Distinguished Dissertation Award in 2016. PDF
NWPT 2016: Thread Summaries for Lock-Free Data Structures. publications
FSTTCS 2016: Summaries for Context-Free Games. publications
D-CON 2017: Roland Meyer will speak at the D-CON workshop.
EATCS Distinguished Dissertation Award: The thesis “Monoids as Storage Mechanisms” (by Georg Zetzsche) received the EATCS Distinguished Dissertation Award in 2016. PDF
Marktoberdorf 2016: Sebastian Wolff was accepted to the Marktoberdorf Summer School.
MEMICS 2016: Roland Meyer will speak at the MEMICS workshop.
Carl Zeiss: Our project ArchiV: Architecture-aware Verification has been granted. research
LICS 2016: Complexity of Regular Abstractions of One-Counter Languages. publications
LICS 2016: First-Order Logic with Reachability for Infinite-State Systems. publications
UPMARC 2016: Roland Meyer will speak at the UPMARC summer school.
CONCUR 2017: Roland Meyer is a co-chair of the conference.
ESOP 2016: On Hierarchical Communication Topologies in the π-calculus. publications
Best teaching award SoSe 2015: Our Bachelor's course Logik received the best teaching award.
VMCAI 2016: Pointer Race Freedom. publications
FSTTCS 2015: What's Decidable about Availability Languages?. publications
RP 2015: The Emptiness Problem for Valence Automata or: Another Decidable Extension of Petri Nets. publications
Best student paper at ICALP 2015: An approach to computing downward closures. publications
ACM TECS: Memory-Model-Aware Testing - a Unified Complexity Analysis. publications
NETYS 2015: Antichains for Recursive Program Verification. publications
CCDP 2015: Roland Meyer will give an invited talk. More about the workshop can be found here.
MM 2015: Roland Meyer will give an invited talk. More about the workshop can be found here.
TACAS 2016: Roland Meyer is a member of the programme committee.
STACS 2015: Computing downward closures for stacked counter automata. publications
CONCUR 2015: Roland Meyer is a member of the programme committee. More about the conference can be found here.
ACSD 2015: Roland Meyer is a co-chair of the programme committee. More about the conference can be found here.
FASE 2015: Lazy TSO Reachability. publications
INFINITY 2014: Roland Meyer will give an invited talk. More about the workshop can be found here.
Best paper at ACSD 2014: Memory-Model-Aware Testing - a Unified Complexity Analysis. publications
CONCUR 2014: Bounds on Mobility. publications
MFCS 2014: The monoid of queue actions. publications
weacon: Research training group Weak Consistency. weacon
ICALP 2014: Robustness against Power is PSPACE-complete. publications
STACS 2014: On Boolean closed full trios and rational Kripke frames. publications
DFG: Our project R2M2: Robustness against Relaxed Memory Models has been granted. research
ACSD 2014: Roland Meyer is a member of the programme committee. More about the conference can be found here.
Best teaching award SoSe 2013: Our Bachelor's course Logik received the best teaching award.
FSTTCS 2013: A Theory of Partitioned Global Address Spaces. publications
LMCS: A Polynomial Translation of Pi-Calculus (FCP) to Safe Petri Nets. publications
MFCS 2013: Semilinearity and Context-Freeness of Languages Accepted by Valence Automata. publications
CONCUR 2013: A Theory of Name Boundedness. publications
ICALP 2013: Rational Subsets and Submonoids of Wreath Products. publications
ICALP 2013: Silent Transitions in Automata with Storage. publications
SAS 2013: Static Provenance Verification for Message Passing Programs. publications
ESOP 2013: Checking and Enforcing Robustness against TSO. publications
TACAS 2014: Roland Meyer is a member of the programme committee. More about the conference can be found here.
DAAD-PROCOPE: Our project ROIS: Robustness under Realistic Instruction Sets has been granted. research
LMCS: Petri Net Reachability Graphs: Decidability Status of FO Properties. publications
ACSD 2013: Roland Meyer is a member of the programme committee. More about the conference can be found here.
Trencher: Our tool for checking robustness against TSO is available for download. Trencher
Best paper at ACSD 2012: An Algorithmic Framework for Coverability in Well-Structured Systems. publications
CONCUR 2012: A Polynomial Translation of Pi-Calculus (FCP) to Safe Petri Nets. publications
Best paper at ETAPS 2012: Language-Theoretic Abstraction Refinement was awarded best paper from EAPLS. publications
YR-CONCUR 2012: Roland Meyer is a member of the programme committee. More about the workshop can be found here.
INFINITY 2012: Roland Meyer is a member of the programme committee. More about the workshop can be found here.
FSTTCS 2011: Petri Net Reachability Graphs: Decidability Status of FO Properties. publications
ACSD 2012: Roland Meyer is a member of the programme committee. More about the conference can be found here.
D-CON 2012: will be organised by the Concurrency Theory Group. The workshop takes place on the 08th and 09th of March 2012. More about the workshop can be found here.
YR-CONCUR 2011: Roland Meyer is a member of the programme committee. More about the workshop can be found here.
Theorietag 2011: Georg is giving an invited talk on erasing productions in grammars with regulated rewriting. Homepage
ICALP 2011: Deciding robustness against total store ordering. publications
ICALP 2011: On the capabilities of grammars, automata and transducers controlled by monoids. publications
DLT 2011: A sufficient condition for erasing productions to be avoidable. publications
ACSD 2011: Roland Meyer is a member of the programme committee. More about the conference can be found here.
CONCUR 2010: Kleene, Rabin, and Scott are available. publications
ICALP 2010: The downward-closure of Petri net languages. publications
CAV 2010: Petruchio: from dynamic networks to nets. publications

Auf diesem Webangebot gilt die Datenschutzerklärung der TU Braunschweig.