Institute of

Theoretical Computer Science

Carl-Friedrich-Gauß-Fakultät

Technische Universität Braunschweig

Thomas Haas

PhD Student

M.Sc. in Computer Science

Email:	t.haas@tu-bs.de
Office:	Informatikzentrum, 3rd floor, office 343 (IZ 343),
	Mühlenpfordtstr. 23, D-38106 Braunschweig
Mail:	Thomas Haas
	Institut für Theoretische Informatik
	Mühlenpfordtstr. 23
	D-38106 Braunschweig
	Germany

List of Publications

Since October 2019 I am a PhD student at the Institute of Theoretical Computer Science in Braunschweig. I graduated from Technische Universität Braunschweig in 2019.

Teaching

2020: Theoretische Informatik II (organizer, tutor)
2019/20: Theoretische Informatik I (organizer, tutor)

Other activities

I did research at the ERATO Project in Tokyo, Japan.

I have attended the following workshops and conferences:

CAV2019 DCON CAV2020

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.