Papers archive | Programming Languages & Verification

Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler.

Heiko Becker, Eva Darulova, Magnus O. Myreen, Zachary Tatlock.
CAV 2019.

Probabilistic Bisimulation for Parameterized Systems - (with Applications to Verifying Anonymous Protocols).

Chih-Duo Hong, Anthony W. Lin, Rupak Majumdar, Philipp Rümmer.
CAV 2019.

Sound Approximation of Programs with Elementary Functions.

Eva Darulova, Anastasia Volkova.
CAV 2019.

Motion Session Types for Robotic Interactions (Brave New Idea Paper).

Rupak Majumdar, Marcus Pirron, Nobuko Yoshida, Damien Zufferey.
ECOOP 2019.

Robustly Safe Compilation.

Marco Patrignani, Deepak Garg.
ESOP 2019.

Formally Verified Roundoff Errors Using SMT-based Certificates and Subdivisions.

Joachim Bard, Heiko Becker, Eva Darulova.
FM 2019.

Evrostos: the rLTL verifier.

Tzanis Anevlavis, Daniel Neider, Matthew Phillipe, Paulo Tabuada.
HSCC 2019.

On the decidability of reachability in linear time-invariant systems.

Nathanaël Fijalkow, Joël Ouaknine, Amaury Pouly, João Sousa Pinto, James Worrell.
HSCC 2019.

On Reachability Problems for Low-Dimensional Matrix Semigroups.

Thomas Colcombet, Joël Ouaknine, Pavel Semukhin, James Worrell.
ICALP 2019.

Termination of Linear Loops over the Integers.

Mehran Hosseini, Joël Ouaknine, James Worrell.
ICALP 2019.

PGCD: robot programming and verification with geometry, concurrency, and dynamics.

Gregor B. Banusic, Rupak Majumdar, Marcus Pirron, Anne-Kathrin Schmuck, Damien Zufferey.
ICCPS 2019.

Programming event processors with thingflow.

Jeffrey M. Fischer, Rupak Majumdar.
ICCPS 2019.

Compositional Synthesis of Finite-State Abstractions.

Kaushik Mallik, Anne-Kathrin Schmuck, Sadegh Soudjani, Rupak Majumdar.
IEEE Trans. Automat. Contr. 2019.

Shrinking Horizon Model Predictive Control With Signal Temporal Logic Constraints Under Stochastic Disturbances.

Samira S. Farahani, Rupak Majumdar, Vinayak S. Prabhu, Sadegh Soudjani.
IEEE Trans. Automat. Contr. 2019.

Differentially testing soundness and precision of program analyzers.

Christian Klinger, Maria Christakis, Valentin Wüstholz.
ISSTA 2019.

On the Decidability of Membership in Matrix-exponential Semigroups.

Joël Ouaknine, Amaury Pouly, João Sousa Pinto, James Worrell.
J. ACM 2019.

Cyclic-routing of Unmanned Aerial Vehicles.

Nir Drucker, Hsi-Ming Ho, Joël Ouaknine, Michal Penn, Ofer Strichman.
J. Comput. Syst. Sci. 2019.

Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests.

Christoph Haase, Georg Zetzsche.
LICS 2019.

On the Expressiveness and Monitoring of Metric Temporal Logic.

Hsi-Ming Ho, Joël Ouaknine, James Worrell.
Logical Methods in Computer Science 2019.

Evaluating Branching Heuristics in Interval Constraint Propagation for Satisfiability.

Calvin Huang, Soonho Kong, Sicun Gao, Damien Zufferey.
NSV@CAV 2019.

Cost-sensitive classifier chains: Selecting low-cost features in multi-label classification.

Pawel Teisseyre, Damien Zufferey, Marta Slomka.
Pattern Recognition 2019.

Bidirectional type checking for relational properties.

Ezgi Çiçek, Weihao Qu, Gilles Barthe, Marco Gaboardi, Deepak Garg.
PLDI 2019.

Model checking for weakly consistent libraries.

Michalis Kokologiannakis, Azalea Raad, Viktor Vafeiadis.
PLDI 2019.

Bridging the gap between programming languages and hardware weak memory models.

Anton Podkopaev, Ori Lahav, Viktor Vafeiadis.
POPL 2019.

Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization.

Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Justin Hsu.
POPL 2019.

From fine- to coarse-grained dynamic information flow control and back.

Marco Vassena, Alejandro Russo, Deepak Garg, Vineet Rajani, Deian Stefan.
POPL 2019.

Grounding thin-air reads with event structures.

Soham Chakraborty, Viktor Vafeiadis.
POPL 2019.

On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models.

Azalea Raad, Marko Doko, Lovro Rozic, Ori Lahav, Viktor Vafeiadis.
POPL 2019.

Checking linearizability using hitting families.

Burcu Kulahcioglu Ozkan, Rupak Majumdar, Filip Niksic.
PPoPP 2019.

Coverability Is Undecidable in One-Dimensional Pushdown Vector Addition Systems with Resets.

Sylvain Schmitz, Georg Zetzsche.
RP 2019.

The Semialgebraic Orbit Problem.

Shaull Almagor, Joël Ouaknine, James Worrell.
STACS 2019.

Environmentally-Friendly GR(1) Synthesis.

Rupak Majumdar, Nir Piterman, Anne-Kathrin Schmuck.
TACAS 2019.

Semantic Fault Localization and Suspiciousness Ranking.

Maria Christakis, Matthias Heizmann, Muhammad Numair Mansur, Christian Schilling, Valentin Wüstholz.
TACAS 2019.

Complete Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem.

Nathanaël Fijalkow, Pierre Ohlmann, Joël Ouaknine, Amaury Pouly, James Worrell.
Theory Comput. Syst. 2019.

On the Semantics of Snapshot Isolation.

Azalea Raad, Ori Lahav, Viktor Vafeiadis.
VMCAI 2019.

Doctoral Thesis: Relational Cost Analysis

Ezgi Çiçek.
Technical Report MPI-SWS-2018-006 2018.

Compositional Synthesis of Piece-Wise Functions by Learning Classifiers.

Daniel Neider, Shambwaditya Saha, P. Madhusudan.
ACM Trans. Comput. Log. 2018.

Reachability analysis of reversal-bounded automata on series-parallel graphs.

Rayna Dimitrova, Rupak Majumdar.
Acta Inf. 2018.

Concentration of Measure for Chance-Constrained Optimization.

Sadegh Soudjani, Rupak Majumdar.
ADHS 2018.

Automatically testing implementations of numerical abstract domains.

Alexandra Bugariu, Valentin Wüstholz, Maria Christakis, Peter Müller.
ASE 2018.

Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility.

Anthony W. Lin, Rupak Majumdar.
ATVA 2018.

Lazy Abstraction-Based Control for Safety Specifications.

Kyle Hsu, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck.
CDC 2018.

Verifying rLTL formulas: now faster than ever before!

Tzanis Anevlavis, Matthew Philippe, Daniel Neider, Paulo Tabuada.
CDC 2018.

CFar: A Tool to Increase Communication, Productivity, and Review Quality in Collaborative Code Reviews.

Austin Z. Henley, KIotavanç Muçlu, Maria Christakis, Scott D. Fleming, Christian Bird.
CHI 2018.

DebugAR: Mixed Dimensional Displays for Immersive Debugging of Distributed Systems.

Patrick Reipschläger, Burcu Kulahcioglu Ozkan, Aman Shankar Mathur, Stefan Gumhold, Rupak Majumdar, Raimund Dachselt.
CHI Extended Abstracts 2018.

Bounded Context Switching for Valence Systems.

Roland Meyer, Sebastian Muskalla, Georg Zetzsche.
CONCUR 2018.

Effective Divergence Analysis for Linear Recurrence Sequences.

Shaull Almagor, Brynmor Chapman, Mehran Hosseini, Joël Ouaknine, James Worrell.
CONCUR 2018.

Verification of Immediate Observation Population Protocols.

Javier Esparza, Pierre Ganty, Rupak Majumdar, Chana Weil-Kennedy.
CONCUR 2018.

Causality Analysis for Concurrent Reactive Systems (Extended Abstract).

Rayna Dimitrova, Rupak Majumdar, Vinayak S. Prabhu.
CREST@ETAPS 2018.

Types for Information Flow Control: Labeling Granularity and Semantic Models.

Vineet Rajani, Deepak Garg.
CSF 2018.

Synthesizing Optimally Resilient Controllers.

Daniel Neider, Alexander Weinert, Martin Zimmermann.
CSL 2018.

Discrete Choice in the Presence of Numerical Uncertainties.

Debasmita Lohar, Eva Darulova, Sylvie Putot, Eric Goubault.
EMSOFT 2018.

Embedded software for robotics: challenges and future directions: special session.

Houssam Abbas, Indranil Saha, Yasser Shoukry, Rüdiger Ehlers, Georgios Fainekos, Rajesh Gupta, Rupak Majumdar, Dogan Ulus.
EMSOFT 2018.

iDeA: an immersive debugger for actors.

Aman Shankar Mathur, Burcu Kulahcioglu Ozkan, Rupak Majumdar.
Erlang Workshop 2018.

A Separation Logic for a Promising Semantics.

Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, Viktor Vafeiadis.
ESOP 2018.

On Parallel Snapshot Isolation and Release/Acquire Consistency.

Azalea Raad, Ori Lahav, Viktor Vafeiadis.
ESOP 2018.

Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus.

Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, Deepak Garg.
ESOP 2018.

Combining Tools for Optimization and Analysis of Floating-Point Computations.

Heiko Becker, Pavel Panchekha, Eva Darulova, Zachary Tatlock.
FM 2018.

A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4.

Heiko Becker, Nikita Zyuzin, Raphaël Monat, Eva Darulova, Magnus O. Myreen, Anthony C. J. Fox.
FMCAD 2018.

Learning Linear Temporal Properties.

Daniel Neider, Ivan Gavran.
FMCAD 2018.

Random Testing for Distributed Systems with Theoretical Guarantees (Invited Paper).

Rupak Majumdar.
FSTTCS 2018.

Model Checking Real-Time Systems.

Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, Joël Ouaknine, James Worrell.
Handbook of Model Checking 2018.

Symbolic Model Checking in Non-Boolean Domains.

Rupak Majumdar, Jean-François Raskin.
Handbook of Model Checking 2018.

Multi-Layered Abstraction-Based Controller Synthesis for Continuous-Time Systems.

Kyle Hsu, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck.
HSCC 2018.

O-Minimal Invariants for Linear Loops.

Shaull Almagor, Dmitry Chistikov, Joël Ouaknine, James Worrell.
ICALP 2018.

Unboundedness Problems for Languages of Vector Addition Systems.

Wojciech Czerwinski, Piotr Hofman, Georg Zetzsche.
ICALP 2018.

Parameter optimization in control software using statistical fault localization techniques.

Jyotirmoy V. Deshmukh, Xiaoqing Jin, Rupak Majumdar, Vinayak S. Prabhu.
ICCPS 2018.

Sound Mixed-Precision Optimization with Rewriting.

Eva Darulova, Einar Horn, Saksham Sharma.
ICCPS 2018.

MoSeL: a general, extensible modal framework for interactive proofs in separation logic.

Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer.
ICFP 2018.

Mtac2: typed tactics for backward reasoning in Coq.

Jan-Oliver Kaiser, Beta Ziliani, Robbert Krebbers, Yann Régis-Gianas, Derek Dreyer.
ICFP 2018.

DroidStar: callback typestates for Android classes.

Arjun Radhakrishna, Nicholas V. Lewchenko, Shawn Meier, Sergio Mover, Krishna Chaitanya Sripada, Damien Zufferey, Bor-Yuh Evan Chang, Pavol Cerný.
ICSE 2018.

Convex Language Semantics for Nondeterministic Probabilistic Automata.

Gerco van Heerdt, Justin Hsu, Joël Ouaknine, Alexandra Silva.
ICTAC 2018.

Discrete Choice in the Presence of Numerical Uncertainties.

Debasmita Lohar, Eva Darulova, Sylvie Putot, Eric Goubault.
IEEE Trans. on CAD of Integrated Circuits and Systems 2018.

GPS $$+$$ + : Reasoning About Fences and Relaxed Atomics.

Mengda He, Viktor Vafeiadis, Shengchao Qin, João F. Ferreira.
International Journal of Parallel Programming 2018.

Iris from the ground up: A modular foundation for higher-order concurrent separation logic.

Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, Derek Dreyer.
J. Funct. Program. 2018.

Polynomial Invariants for Affine Programs.

Ehud Hrushovski, Joël Ouaknine, Amaury Pouly, James Worrell.
LICS 2018.

Separability by piecewise testable languages and downward closures beyond subwords.

Georg Zetzsche.
LICS 2018.

Sequential Relational Decomposition.

Dror Fried, Axel Legay, Joël Ouaknine, Moshe Y. Vardi.
LICS 2018.

Model Checking Flat Freeze LTL on One-Counter Automata.

Antonia Lechner, Richard Mayr, Joël Ouaknine, Amaury Pouly, James Worrell.
Logical Methods in Computer Science 2018.

Benchmarks for Automata Learning and Conformance Testing.

Daniel Neider, Rick Smetsers, Frits W. Vaandrager, Harco Kuppens.
Models, Mindsets, Meta 2018.

Tᴏᴏʟ: accessible automated reasoning for human robot collaboration.

Ivan Gavran, Ortwin Mailahn, Rainer Müller, Richard Peifer, Damien Zufferey.
Onward! 2018.

Horn-ICE learning for synthesizing invariants and contracts.

P. Ezudheen, Daniel Neider, Deepak D'Souza, Pranav Garg, P. Madhusudan.
OOPSLA 2018.

Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model.

Azalea Raad, Viktor Vafeiadis.
OOPSLA 2018.

Randomized testing of distributed systems with probabilistic guarantees.

Burcu Kulahcioglu Ozkan, Rupak Majumdar, Filip Niksic, Mitra Tabaei Befrouei, Georg Weissenbacher.
OOPSLA 2018.

Effective stateless model checking for C/C++ concurrency.

Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, Viktor Vafeiadis.
POPL 2018.

Monadic refinements for relational cost analysis.

Ivan Radicek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Florian Zuleger.
POPL 2018.

Parametricity versus the universal type.

Dominique Devriese, Marco Patrignani, Frank Piessens.
POPL 2018.

RustBelt: securing the foundations of the rust programming language.

Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer.
POPL 2018.

Why is random testing effective for partition tolerance bugs?

Rupak Majumdar, Filip Niksic.
POPL 2018.

Approximate Time Bounded Reachability for CTMCs and CTMDPs: A Lyapunov Approach.

Mahmoud Salamati, Sadegh Soudjani, Rupak Majumdar.
QEST 2018.

Knapsack Problems for Wreath Products.

Moses Ganardi, Daniel König, Markus Lohrey, Georg Zetzsche.
STACS 2018.

Daisy - Framework for Analysis and Optimization of Numerical Programs (Tool Paper).

Eva Darulova, Anastasiia Izycheva, Fariha Nasir, Fabian Ritter, Heiko Becker, Robert Bastian.
TACAS 2018.

Invariant Synthesis for Incomplete Verification Engines.

Daniel Neider, Pranav Garg, P. Madhusudan, Shambwaditya Saha, Daejun Park.
TACAS 2018.

Shrinking Horizon Model Predictive Control with chance-constrained signal temporal logic specifications.

Samira S. Farahani, Rupak Majumdar, Vinayak S. Prabhu, Sadegh Esmaeil Zadeh Soudjani.
ACC 2017.

Towards a Compiler for Reals.

Eva Darulova, Viktor Kuncak.
ACM TOPLAS 2017.

Antlab: A Multi-Robot Task Server.

Ivan Gavran, Rupak Majumdar, Indranil Saha.
ACM Trans. Embedded Comput. Syst. 2017.

Testing Cyber-Physical Systems through Bayesian Optimization.

Jyotirmoy V. Deshmukh, Marko Horvat, Xiaoqing Jin, Rupak Majumdar, Vinayak S. Prabhu.
ACM Trans. Embedded Comput. Syst. 2017.

Approximate counting in SMT and value estimation for probabilistic programs.

Dmitry Chistikov, Rayna Dimitrova, Rupak Majumdar.
Acta Inf. 2017.

Dynamic Bayesian networks for formal verification of structured stochastic processes.

Sadegh Esmaeil Zadeh Soudjani, Alessandro Abate, Rupak Majumdar.
Acta Inf. 2017.

Verification of population protocols.

Javier Esparza, Pierre Ganty, Jérôme Leroux, Rupak Majumdar.
Acta Inf. 2017.

Synthesis of Problems for Shaded Area Geometry Reasoning.

Chris Alvin, Sumit Gulwani, Rupak Majumdar, Supratik Mukhopadhyay.
AIED 2017.

Program Verification Under Weak Memory Consistency Using Separation Logic.

Viktor Vafeiadis.
CAV 2017.

Compositional abstractions of interconnected discrete-time stochastic control systems.

Abolfazl Lavaei, Sadegh Esmaeil Zadeh Soudjani, Rupak Majumdar, Majid Zamani.
CDC 2017.

Compositional construction of finite state abstractions for stochastic control systems.

Kaushik Mallik, Sadegh Esmaeil Zadeh Soudjani, Anne-Kathrin Schmuck, Rupak Majumdar.
CDC 2017.

Formalizing the concurrency semantics of an LLVM fragment.

Soham Chakraborty, Viktor Vafeiadis.
CGO 2017.

The Robot Routing Problem for Collecting Aggregate Stochastic Rewards.

Rayna Dimitrova, Ivan Gavran, Rupak Majumdar, Vinayak S. Prabhu, Sadegh Esmaeil Zadeh Soudjani.
CONCUR 2017.

Dynamic hierarchical reactive controller synthesis.

Anne-Kathrin Schmuck, Rupak Majumdar, Adrian Leva.
Discrete Event Dynamic Systems 2017.

A Characterization for Decidable Separability by Piecewise Testable Languages.

Wojciech Czerwinski, Wim Martens, Lorijn van Rooijen, Marc Zeitoun, Georg Zetzsche.
Discrete Mathematics & Theoretical Computer Science 2017.

Promising Compilation to ARMv8 POP.

Anton Podkopaev, Ori Lahav, Viktor Vafeiadis.
ECOOP 2017.

Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris.

Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis.
ECOOP 2017.

Failure-directed program trimming.

Kostas Ferles, Valentin Wüstholz, Maria Christakis, Isil Dillig.
ESEC/SIGSOFT FSE 2017.

Tackling Real-Life Relaxed Concurrency with FSL++.

Marko Doko, Viktor Vafeiadis.
ESOP 2017.

The Essence of Higher-Order Concurrent Separation Logic.

Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal.
ESOP 2017.

Synthesis of Solutions for Shaded Area Geometry Problems.

Chris Alvin, Sumit Gulwani, Rupak Majumdar, Supratik Mukhopadhyay.
FLAIRS Conference 2017.

FAR-Cubicle - A new reachability algorithm for Cubicle.

Sylvain Conchon, Amit Goel, Sava Krstic, Rupak Majumdar, Mattias Roux.
FMCAD 2017.

On sound relative error bounds for floating-point arithmetic.

Anastasiia Izycheva, Eva Darulova.
FMCAD 2017.

Model checking parameterized asynchronous shared-memory systems.

Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, Rupak Majumdar.
Formal Methods in System Design 2017.

Quantifying conformance using the Skorokhod metric.

Jyotirmoy V. Deshmukh, Rupak Majumdar, Vinayak S. Prabhu.
Formal Methods in System Design 2017.

Deferrability Analysis for JavaScript.

Johannes Kloos, Rupak Majumdar, Frank McCabe.
Haifa Verification Conference 2017.

Controller Synthesis for Reward Collecting Markov Processes in Continuous Space.

Sadegh Esmaeil Zadeh Soudjani, Rupak Majumdar.
HSCC 2017.

On the Polytope Escape Problem for Continuous Linear Dynamical Systems.

Joël Ouaknine, João Sousa Pinto, James Worrell.
HSCC 2017.

The Polytope-Collision Problem.

Shaull Almagor, Joël Ouaknine, James Worrell.
ICALP 2017.

A relational logic for higher-order programs.

Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub.
ICFP 2017.

A general framework for dynamic stub injection.

Maria Christakis, Patrick Emmisberger, Patrice Godefroid, Peter Müller.
ICSE 2017.

On parametric timed automata and one-counter machines.

Daniel Bundala, Joël Ouaknine.
Inf. Comput. 2017.

On narrowing the gap between verification and systematic testing.

Maria Christakis.
it - Information Technology 2017.

Decidability, complexity, and expressiveness of first-order logic over the subword ordering.

Simon Halfon, Philippe Schnoebelen, Georg Zetzsche.
LICS 2017.

Programming by Composing Filters.

Jeffrey Fischer, Rupak Majumdar.
LPAR 2017.

Timed Temporal Logics.

Patricia Bouyer, François Laroussinie, Nicolas Markey, Joël Ouaknine, James Worrell.
Models, Algorithms, Logics and Tools 2017.

Robust and compositional verification of object capability patterns.

David Swasey, Deepak Garg, Derek Dreyer.
OOPSLA 2017.

Repairing sequential consistency in C/C++11.

Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer.
PLDI 2017.

A promising semantics for relaxed-memory concurrency.

Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer.
POPL 2017.

Relational cost analysis.

Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Jan Hoffmann.
POPL 2017.

Thread modularity at many levels: a pearl in compositional verification.

Jochen Hoenicke, Rupak Majumdar, Andreas Podelski.
POPL 2017.

Multilevel Monte Carlo Method for Statistical Model Checking of Hybrid Systems.

Sadegh Esmaeil Zadeh Soudjani, Rupak Majumdar, Tigran Nagapetyan.
QEST 2017.

Type systems for information flow control: the question of granularity.

Vineet Rajani, Iulia Bastys, Willard Rafnsson, Deepak Garg.
SIGLOG News 2017.

Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem.

Nathanaël Fijalkow, Pierre Ohlmann, Joël Ouaknine, Amaury Pouly, James Worrell.
STACS 2017.

Fair Termination for Parameterized Probabilistic Concurrent Systems.

Ondrej Lengál, Anthony Widjaja Lin, Rupak Majumdar, Philipp Rümmer.
TACAS 2017.

On Boolean Closed Full Trios and Rational Kripke Frames.

Georg Zetzsche, Dietrich Kuske, Markus Lohrey.
Theory Comput. Syst. 2017.

Type Systems for Information Flow Control: The Question of Granularity

Vineet Rajani, Iulia Bastys, Willard Rafnsson, Deepak Garg.
Technical Report MPI-SWS-2016-012 2016.

Repairing Sequential Consistency in C/C++11

Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer.
Technical Report MPI-SWS-2016-011 2016.

Hitting Families of Schedules for Asynchronous Programs.

Dmitry Chistikov, Rupak Majumdar, Filip Niksic.
CAV 2016.

Algorithms and Tools for Verification and Testing of Asynchronous Programs

Zilong Wang.
Technical Report MPI-SWS-2016-001 2016.

What developers want and need from program analysis: an empirical study.

Maria Christakis, Christian Bird.
ASE 2016.

Symbolic Model Checking for Factored Probabilistic Models.

David Deininger, Rayna Dimitrova, Rupak Majumdar.
ATVA 2016.

Monoids as Storage Mechanisms.

Georg Zetzsche.
Bulletin of the EATCS 2016.

Synthesis of safety controllers robust to unmodeled intermittent disturbances.

Eric Dallal, Daniel Neider, Paulo Tabuada.
CDC 2016.

Validating optimizations of concurrent C/C++ programs.

Soham Chakraborty, Viktor Vafeiadis.
CGO 2016.

Causally Consistent Dynamic Slicing

Roly Perera, Deepak Garg, James Cheney.
CONCUR 2016.

Model Checking Flat Freeze LTL on One-Counter Automata.

Antonia Lechner, Richard Mayr, Joël Ouaknine, Amaury Pouly, James Worrell.
CONCUR 2016.

On Modular and Fully-Abstract Compilation.

Marco Patrignani, Dominique Devriese, Frank Piessens.
CSF 2016.

Robust Linear Temporal Logic.

Paulo Tabuada, Daniel Neider.
CSL 2016.

Explaining Relaxed Memory Models with Program Transformations.

Ori Lahav, Viktor Vafeiadis.
FM 2016.

Model Checking Population Protocols.

Javier Esparza, Pierre Ganty, Jérôme Leroux, Rupak Majumdar.
FSTTCS 2016.

Proving the Herman-Protocol Conjecture.

Maria Bruna, Radu Grigore, Stefan Kiefer, Joël Ouaknine, James Worrell.
ICALP 2016.

The Complexity of Downward Closure Comparisons.

Georg Zetzsche.
ICALP 2016.

A type theory for incremental computational complexity with control flow changes

Ezgi Çiçek, Zoe Paraskevopoulou, Deepak Garg.
ICFP 2016.

Higher-order ghost state.

Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer.
ICFP 2016.

Guiding dynamic symbolic execution toward unverified program executions.

Maria Christakis, Peter Müller, Valentin Wüstholz.
ICSE 2016.

Parameterized Verification of Asynchronous Shared-Memory Systems.

Javier Esparza, Pierre Ganty, Rupak Majumdar.
J. ACM 2016.

First-order logic with reachability for infinite-state systems.

Emanuele D'Osualdo, Roland Meyer, Georg Zetzsche.
LICS 2016.

On Recurrent Reachability for Continuous Linear Dynamical Systems.

Ventsislav Chonev, Joël Ouaknine, James Worrell.
LICS 2016.

Solvability of Matrix-Exponential Equations.

Joël Ouaknine, Amaury Pouly, João Sousa Pinto, James Worrell.
LICS 2016.

The complexity of regular abstractions of one-counter languages.

Mohamed Faouzi Atig, Dmitry Chistikov, Piotr Hofman, K. Narayan Kumar, Prakash Saivasan, Georg Zetzsche.
LICS 2016.

Monoids as Storage Mechanisms.

Georg Zetzsche.
Monoids as Storage Mechanisms. 2016.

Reasoning about Fences and Relaxed Atomics.

Mengda He, Viktor Vafeiadis, Shengchao Qin, João F. Ferreira.
PDP 2016.

Fully-abstract compilation by approximate back-translation.

Dominique Devriese, Marco Patrignani, Frank Piessens.
POPL 2016.

Learning invariants using decision trees and implication counterexamples.

Pranav Garg, Daniel Neider, P. Madhusudan, Dan Roth.
POPL 2016.

Lightweight verification of separate compilation.

Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis.
POPL 2016.

PSync: a partially synchronous language for fault-tolerant distributed algorithms.

Cezara Dragoi, Thomas A. Henzinger, Damien Zufferey.
POPL 2016.

Taming release-acquire consistency.

Ori Lahav, Nick Giannarakis, Viktor Vafeiadis.
POPL 2016.

Bounded Abstract Interpretation.

Maria Christakis, Valentin Wüstholz.
SAS 2016.

LLSPLAT: Improving Concolic Testing by Bounded Model Checking.

Min Gao, Lei He, Rupak Majumdar, Zilong Wang.
SCAM 2016.

Abstract Learning Frameworks for Synthesis.

Christof Löding, P. Madhusudan, Daniel Neider.
TACAS 2016.

An Automaton Learning Approach to Solving Safety Games over Infinite Graphs.

Daniel Neider, Ufuk Topcu.
TACAS 2016.

Integrated Environment for Diagnosing Verification Errors.

Maria Christakis, K. Rustan M. Leino, Peter Müller, Valentin Wüstholz.
TACAS 2016.

Interpolants in Nonlinear Theories Over the Reals.

Sicun Gao, Damien Zufferey.
TACAS 2016.

Partial Order Reduction for Event-Driven Multi-threaded Programs.

Pallavi Maiya, Rahul Gupta, Aditya Kanade, Rupak Majumdar.
TACAS 2016.

Probabilistic CTL: The Deductive Way.

Rayna Dimitrova, Luis María Ferrer Fioriti, Holger Hermanns, Rupak Majumdar.
TACAS 2016.

Robots at the Edge of the Cloud.

Rupak Majumdar.
TACAS 2016.

Safety Verification of Continuous-Space Pure Jump Markov Processes.

Sadegh Esmaeil Zadeh Soudjani, Rupak Majumdar, Alessandro Abate.
TACAS 2016.

Synthesizing Piece-Wise Functions by Learning Classifiers.

Daniel Neider, Shambwaditya Saha, P. Madhusudan.
TACAS 2016.

A Program Logic for C11 Memory Fences.

Marko Doko, Viktor Vafeiadis.
VMCAI 2016.

Doctoral Thesis: Interactive Typed Tactic Programming in the Coq Proof Assistant

Beta Ziliani.
Technical Report MPI-SWS-2015-001 2015.

Bbs: A Phase-Bounded Model Checker for Asynchronous Programs.

Rupak Majumdar, Zilong Wang.
CAV 2015.

Model Checking Parameterized Asynchronous Shared-Memory Systems.

Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, Rupak Majumdar.
CAV 2015.

Model Checking Parameterized Asynchronous Shared-Memory Systems.

Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, Rupak Majumdar.
CAV 2015.

Quantifying Conformance Using the Skorokhod Metric.

Jyotirmoy V. Deshmukh, Rupak Majumdar, Vinayak S. Prabhu.
CAV 2015.

Dynamic Bayesian Networks as Formal Abstractions of Structured Stochastic Processes.

Sadegh Esmaeil Zadeh Soudjani, Alessandro Abate, Rupak Majumdar.
CONCUR 2015.

Rely/Guarantee Reasoning for Asynchronous Programs.

Ivan Gavran, Filip Niksic, Aditya Kanade, Rupak Majumdar, Viktor Vafeiadis.
CONCUR 2015.

Verification of Population Protocols.

Javier Esparza, Pierre Ganty, Jérôme Leroux, Rupak Majumdar.
CONCUR 2015.

Formal Reasoning about the C11 Weak Memory Model.

Viktor Vafeiadis.
CPP 2015.

Proving Lock-Freedom Easily and Automatically.

Xiao Jia, Wei Li, Viktor Vafeiadis.
CPP 2015.

Modular Verification of Concurrency-Aware Linearizability.

Nir Hemed, Noam Rinetzky, Viktor Vafeiadis.
DISC 2015.

Asynchronous Liquid Separation Types.

Johannes Kloos, Rupak Majumdar, Viktor Vafeiadis.
ECOOP 2015.

Analysis of Asynchronous Programs with Event-Based Synchronization.

Michael Emmi, Pierre Ganty, Rupak Majumdar, Fernando Rosa-Velardo.
ESOP 2015.

Refinement Types for Incremental Computational Complexity

Ezgi Çiçek, Deepak Garg, Umut A. Acar.
ESOP 2015.

Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists.

Pranav Garg, Christof Löding, P. Madhusudan, Daniel Neider.
Formal Methods in System Design 2015.

Reachability Analysis of Reversal-bounded Automata on Series-Parallel Graphs.

Rayna Dimitrova, Rupak Majumdar.
GandALF 2015.

Dynamic scheduling for networked control systems.

Indranil Saha, Sanjoy Baruah, Rupak Majumdar.
HSCC 2015.

An Approach to Computing Downward Closures.

Georg Zetzsche.
ICALP 2015.

Owicki-Gries Reasoning for Weak Memory Models.

Ori Lahav, Viktor Vafeiadis.
ICALP 2015.

Pilsner: a compositionally verified compiler for a higher-order imperative language.

Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, Viktor Vafeiadis.
ICFP 2015.

Mtac: A monad for typed tactic programming in Coq.

Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis.
J. Funct. Program. 2015.

Aspect-oriented linearizability proofs.

Soham Chakraborty, Thomas A. Henzinger, Ali Sezgin, Viktor Vafeiadis.
Logical Methods in Computer Science 2015.

A formal C memory model supporting integer-pointer casts.

Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, Viktor Vafeiadis.
PLDI 2015.

Verifying read-copy-update in a logic for weak memory.

Joseph Tassarotti, Derek Dreyer, Viktor Vafeiadis.
PLDI 2015.

Separation logic for weak memory models.

Viktor Vafeiadis.
PLMW@POPL 2015.

Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it.

Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, Francesco Zappa Nardelli.
POPL 2015.

Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning.

Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, Derek Dreyer.
POPL 2015.

The Emptiness Problem for Valence Automata or: Another Decidable Extension of Petri Nets.

Georg Zetzsche.
RP 2015.

The Need for Language Support for Fault-Tolerant Distributed Systems.

Cezara Dragoi, Thomas A. Henzinger, Damien Zufferey.
SNAPL 2015.

On Termination of Integer Linear Loops.

Joël Ouaknine, João Sousa Pinto, James Worrell.
SODA 2015.

The Polyhedron-Hitting Problem.

Ventsislav Chonev, Joël Ouaknine, James Worrell.
SODA 2015.

IC-Cut: A Compositional Search Strategy for Dynamic Test Generation.

Maria Christakis, Patrice Godefroid.
SPIN 2015.

Computing Downward Closures for Stacked Counter Automata.

Georg Zetzsche.
STACS 2015.

Approximate Counting in SMT and Value Estimation for Probabilistic Programs.

Dmitry Chistikov, Rayna Dimitrova, Rupak Majumdar.
TACAS 2015.

An Experimental Evaluation of Deliberate Unsoundness in a Static Program Analyzer.

Maria Christakis, Peter Müller, Valentin Wüstholz.
VMCAI 2015.

Proving Memory Safety of the ANI Windows Image Parser Using Compositional Exhaustive Testing.

Maria Christakis, Patrice Godefroid.
VMCAI 2015.

GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation

Aaron Turon, Viktor Vafeiadis, Derek Dreyer.
Technical Report MPI-SWS-2014-004 2014.

A Logical Step Forward in Parametric Bisimulations

Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis.
Technical Report MPI-SWS-2014-003 2014.

Synthesis of Geometry Proof Problems.

Chris Alvin, Sumit Gulwani, Rupak Majumdar, Supratik Mukhopadhyay.
AAAI 2014.

Applications of automata learning in verification and synthesis.

Daniel Neider.
Applications of automata learning in verification and synthesis. 2014.

An SMT-Based Approach to Coverability Analysis.

Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp J. Meyer, Filip Niksic.
CAV 2014.

Automating Separation Logic with Trees and Data.

Ruzica Piskac, Thomas Wies, Damien Zufferey.
CAV 2014.

ICE: A Robust Framework for Learning Invariants.

Pranav Garg, Christof Löding, P. Madhusudan, Daniel Neider.
CAV 2014.

Regression Test Selection for Distributed Software Histories.

Milos Gligoric, Rupak Majumdar, Rohan Sharma, Lamyaa Eloussi, Darko Marinov.
CAV 2014.

Temporal Mode-Checking for Runtime Monitoring of Privacy Policies

Omar Chowdhury, Limin Jia, Deepak Garg, Anupam Datta.
CAV 2014.

Bounds on Mobility.

Reiner Hüchting, Rupak Majumdar, Roland Meyer.
CONCUR 2014.

Verification of Cyber-Physical Systems (Dagstuhl Seminar 14122).

Rupak Majumdar, Richard M. Murray, Pavithra Prabhakar.
Dagstuhl Reports 2014.

Deductive control synthesis for alternating-time logics.

Rayna Dimitrova, Rupak Majumdar.
EMSOFT 2014.

Dynamic Package Interfaces.

Shahram Esmaeilsabzali, Rupak Majumdar, Thomas Wies, Damien Zufferey.
FASE 2014.

Formalizing and Verifying a Modern Build Language.

Maria Christakis, K. Rustan M. Leino, Wolfram Schulte.
FM 2014.

Kuai: A model checker for software-defined networks.

Rupak Majumdar, Sai Deep Tetali, Zilong Wang.
FMCAD 2014.

Edit distance for timed automata.

Krishnendu Chatterjee, Rasmus Ibsen-Jensen, Rupak Majumdar.
HSCC 2014.

On the Complexity of Temporal-Logic Path Checking.

Daniel Bundala, Joël Ouaknine.
ICALP 2014.

On the Positivity Problem for Simple Linear Recurrence Sequences, .

Joël Ouaknine, James Worrell.
ICALP 2014.

Ultimate Positivity is Decidable for Simple Linear Recurrence Sequences.

Joël Ouaknine, James Worrell.
ICALP 2014.

Unary Pushdown Automata and Straight-Line Programs.

Dmitry Chistikov, Rupak Majumdar.
ICALP 2014.

Symbolic Control of Stochastic Systems via Approximately Bisimilar Finite Abstractions.

Majid Zamani, Peyman Mohajerin Esfahani, Rupak Majumdar, Alessandro Abate, John Lygeros.
IEEE Trans. Automat. Contr. 2014.

Towards Robustness for Cyber-Physical Systems.

Paulo Tabuada, Sina Yamac Caliskan, Matthias Rungger, Rupak Majumdar.
IEEE Trans. Automat. Contr. 2014.

F-ing modules.

Andreas Rossberg, Claudio V. Russo, Derek Dreyer.
J. Funct. Program. 2014.

Advances in Parametric Real-Time Reasoning.

Daniel Bundala, Joël Ouaknine.
MFCS 2014.

GPS: navigating weak memory with ghosts, protocols, and separation.

Aaron Turon, Viktor Vafeiadis, Derek Dreyer.
OOPSLA 2014.

Race detection for Android applications.

Pallavi Maiya, Aditya Kanade, Rupak Majumdar.
PLDI 2014.

Backpack: retrofitting Haskell with interfaces.

Scott Kilpatrick, Derek Dreyer, Simon L. Peyton Jones, Simon Marlow.
POPL 2014.

Sound Compilation of Reals

Eva Darulova, Viktor Kuncak.
POPL 2014.

Dynamic Test Generation with Static Fields and Initializers.

Maria Christakis, Patrick Emmisberger, Peter Müller.
RV 2014.

Synthesizing Parameterized Unit Tests to Detect Object Invariant Violations.

Maria Christakis, Peter Müller, Valentin Wüstholz.
SEFM 2014.

Positivity Problems for Low-Order Linear Recurrence Sequences.

Joël Ouaknine, James Worrell.
SODA 2014.

Foundations of Infinite-State Verification.

Rupak Majumdar.
Software Systems Safety 2014.

On Boolean closed full trios and rational Kripke frames.

Markus Lohrey, Georg Zetzsche.
STACS 2014.

GRASShopper - Complete Heap Verification with Mixed Specifications.

Ruzica Piskac, Thomas Wies, Damien Zufferey.
TACAS 2014.

Down the Borel hierarchy: Solving Muller games via safety games.

Daniel Neider, Roman Rabinovich, Martin Zimmermann.
Theor. Comput. Sci. 2014.

A Logic-Based Framework for Verifying Consensus Algorithms.

Cezara Dragoi, Thomas A. Henzinger, Helmut Veith, Josef Widder, Damien Zufferey.
VMCAI 2014.

Concurrent Self-Explaining Computation

Roly Perera, Deepak Garg, Umut Acar.
Technical Report MPI-SWS-2013-004 2013.

Dependent Type Theory for Verification of Information Flow and Access Control Policies

Aleksandar Nanevski, Anindya Banerjee, Deepak Garg.
ACM TOPLAS 2013.

Mixin' Up the ML Module System.

Andreas Rossberg, Derek Dreyer.
ACM TOPLAS 2013.

A theory of robust omega-regular software synthesis.

Rupak Majumdar, Elaine Render, Paulo Tabuada.
ACM Trans. Embedded Comput. Syst. 2013.

Automating Separation Logic Using SMT.

Ruzica Piskac, Thomas Wies, Damien Zufferey.
CAV 2013.

Incremental, Inductive Coverability.

Johannes Kloos, Rupak Majumdar, Filip Niksic, Ruzica Piskac.
CAV 2013.

Learning Universally Quantified Invariants of Linear Data Structures.

Pranav Garg, Christof Löding, P. Madhusudan, Daniel Neider.
CAV 2013.

Parameterized Verification of Asynchronous Shared-Memory Systems.

Javier Esparza, Pierre Ganty, Rupak Majumdar.
CAV 2013.

The first workshop on language support for privacy-enhancing technologies (PETShop'13).

Martin Franz, Andreas Holzer, Rupak Majumdar, Bryan Parno, Helmut Veith.
CCS 2013.

Bisimilar finite abstractions of stochastic control systems.

Majid Zamani, Peyman Mohajerin Esfahani, Rupak Majumdar, Alessandro Abate, John Lygeros.
CDC 2013.

Compositional equivalence checking for models and code of control systems.

Rupak Majumdar, Indranil Saha, Koichi Ueda, Hakan Yazarel.
CDC 2013.

A Uniformization Theorem for Nested Word to Word Transductions.

Dmitry Chistikov, Rupak Majumdar.
CIAA 2013.

A Theory of Name Boundedness.

Reiner Hüchting, Rupak Majumdar, Roland Meyer.
CONCUR 2013.

Aspect-Oriented Linearizability Proofs.

Thomas A. Henzinger, Ali Sezgin, Viktor Vafeiadis.
CONCUR 2013.

Expand, Enlarge, and Check for Branching Vector Addition Systems.

Rupak Majumdar, Zilong Wang.
CONCUR 2013.

Internalizing Relational Parametricity in the Extensional Calculus of Constructions.

Neelakantan R. Krishnaswami, Derek Dreyer.
CSL 2013.

Supervisor synthesis for controller upgrades.

Johannes Kloos, Rupak Majumdar.
DATE 2013.

Synthesis of Fixed-point Programs

Eva Darulova, Viktor Kuncak, Rupak Majumdar, Indranil Saha.
EMSOFT 2013.

Code aware resource management.

Krishnendu Chatterjee, Luca de Alfaro, Marco Faella, Rupak Majumdar, Vishwanath Raman.
Formal Methods in System Design 2013.

Specification and Verification of Linear Dynamical Systems: Advances and Challenges.

Joël Ouaknine.
FroCos 2013.

A Theory of Partitioned Global Address Spaces.

Georgel Calin, Egor Derevenetc, Rupak Majumdar, Roland Meyer.
FSTTCS 2013.

Silent Transitions in Automata with Storage.

Georg Zetzsche.
ICALP 2013.

Mtac: a monad for typed tactic programming in Coq.

Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis.
ICFP 2013.

Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency.

Aaron Turon, Derek Dreyer, Lars Birkedal.
ICFP 2013.

Systematic Testing for Detecting Concurrency Errors in Erlang Programs.

Maria Christakis, Alkis Gotovos, Konstantinos Sagonas.
ICST 2013.

The Complexity of Coverage.

Krishnendu Chatterjee, Luca de Alfaro, Rupak Majumdar.
Int. J. Found. Comput. Sci. 2013.

Adjustable References.

Viktor Vafeiadis.
ITP 2013.

CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency.

Jaroslav Sevcík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell.
J. ACM 2013.

How to make ad hoc proof automation less ad hoc.

Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer.
J. Funct. Program. 2013.

Discrete Linear Dynamical Systems.

Joël Ouaknine.
LATA 2013.

Semilinearity and Context-Freeness of Languages Accepted by Valence Automata.

P. Buckheister, Georg Zetzsche.
MFCS 2013.

Regular Model Checking Using Solver Technologies and Automata Learning.

Daniel Neider, Nils Jansen.
NASA Formal Methods 2013.

MrCrypt: static analysis for secure cloud computations.

Sai Deep Tetali, Mohsen Lesani, Rupak Majumdar, Todd D. Millstein.
OOPSLA 2013.

Relaxed separation logic: a program logic for C11 concurrency.

Viktor Vafeiadis, Chinmay Narayan.
OOPSLA 2013.

P: safe asynchronous event-driven programming.

Ankush Desai, Vivek Gupta, Ethan K. Jackson, Shaz Qadeer, Sriram K. Rajamani, Damien Zufferey.
PLDI 2013.

Logical relations for fine-grained concurrency.

Aaron Joseph Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, Derek Dreyer.
POPL 2013.

The power of parameterization in coinductive proof.

Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis.
POPL 2013.

Provenance Verification.

Rupak Majumdar, Roland Meyer, Zilong Wang.
RP 2013.

Static Provenance Verification for Message Passing Programs.

Rupak Majumdar, Roland Meyer, Zilong Wang.
SAS 2013.

Decision Problems for Linear Recurrence Sequences.

Joël Ouaknine.
SCSS 2013.

From tests to proofs.

Ashutosh Gupta, Rupak Majumdar, Andrey Rybalchenko.
STTT 2013.

Backstepping controller synthesis and characterizations of incremental stability.

Majid Zamani, Nathan van de Wouw, Rupak Majumdar.
Systems & Control Letters 2013.

Model Checking Database Applications.

Milos Gligoric, Rupak Majumdar.
TACAS 2013.

Structural Counter Abstraction.

Kshitij Bansal, Eric Koskinen, Thomas Wies, Damien Zufferey.
TACAS 2013.

A Programming Language Approach to Fault Tolerance for Fork-Join Parallelism.

Mustafa Zengin, Viktor Vafeiadis.
TASE 2013.

Functional Programs that Explain their Work

Roly Perera, Umut A. Acar, James Cheney, Paul Blain Levy.
Technical Report MPI-SWS-2012-003 2012.

The Transitive Composability of Relation Transition Systems

Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis.
Technical Report MPI-SWS-2012-002 2012.

The Impact of Higher-Order State and Control Effects on Local Relational Reasoning

Derek Dreyer, Georg Neis, Lars Birkedal.
Technical Report MPI-SWS-2012-001 2012.

Algorithmic verification of asynchronous programs.

Pierre Ganty, Rupak Majumdar.
ACM TOPLAS 2012.

Computing Minimal Separating DFAs and Regular Invariants Using SAT and SMT Solvers.

Daniel Neider.
ATVA 2012.

Equivalence of Games with Probabilistic Uncertainty and Partial-Observation Games.

Krishnendu Chatterjee, Martin Chmelik, Rupak Majumdar.
ATVA 2012.

Approximately Bisimilar Symbolic Models for Digital Control Systems.

Rupak Majumdar, Majid Zamani.
CAV 2012.

Games and Decisions for Rigorous Systems Engineering (Dagstuhl Seminar 12461).

Nikolaj Bjørner, Krishnendu Chatterjee, Laura Kovács, Rupak Majumdar.
Dagstuhl Reports 2012.

Input-output robustness for discrete systems.

Paulo Tabuada, Ayca Balkan, Sina Y. Caliskan, Yasser Shoukry, Rupak Majumdar.
EMSOFT 2012.

Synthesis of minimal-error control software.

Rupak Majumdar, Indranil Saha, Majid Zamani.
EMSOFT 2012.

Trigger memoization in self-triggered control.

Indranil Saha, Rupak Majumdar.
EMSOFT 2012.

Language-Theoretic Abstraction Refinement.

Zhenyue Long, Georgel Calin, Rupak Majumdar, Roland Meyer.
FASE 2012.

Collaborative Verification and Testing with Explicit Assumptions.

Maria Christakis, Peter Müller, Valentin Wüstholz.
FM 2012.

Bounded underapproximations.

Pierre Ganty, Rupak Majumdar, Benjamin Monmege.
Formal Methods in System Design 2012.

Down the Borel Hierarchy: Solving Muller Games via Safety Games

Daniel Neider, Roman Rabinovich, Martin Zimmermann.
GandALF 2012.

Superficially substructural types

Neelakantan R. Krishnaswami, Aaron Turon, Derek Dreyer, Deepak Garg.
ICFP 2012.

Discounting and Averaging in Games across Time scales.

Krishnendu Chatterjee, Rupak Majumdar.
Int. J. Found. Comput. Sci. 2012.

Learning Minimal Deterministic Automata from Inexperienced Teachers.

Martin Leucker, Daniel Neider.
ISoLA 2012.

Machine learning approaches for electric appliance classification.

Damien Zufferey, Christophe Gisler, Omar Abou Khaled, Jean Hennebert.
ISSPA 2012.

The impact of higher-order state and control effects on local relational reasoning.

Derek Dreyer, Georg Neis, Lars Birkedal.
J. Funct. Program. 2012.

A Perfect Model for Bounded Verification.

Javier Esparza, Pierre Ganty, Rupak Majumdar.
LICS 2012.

Countermodels from Sequent Calculi in Multi-Modal Logics

Deepak Garg, Valerio Genovese, Sara Negri.
LICS 2012.

CLSE: Closed-Loop Symbolic Execution.

Rupak Majumdar, Indranil Saha, K. C. Shashidhar, Zilong Wang.
NASA Formal Methods 2012.

Engage: a deployment management system.

Jeffrey Fischer, Rupak Majumdar, Shahram Esmaeilsabzali.
PLDI 2012.

The marriage of bisimulations and Kripke logical relations.

Chung-Kil Hur, Derek Dreyer, Georg Neis, Viktor Vafeiadis.
POPL 2012.

Certifying Solutions for Numerical Constraints

Eva Darulova, Viktor Kuncak.
RV 2012.

Efficient May Happen in Parallel Analysis for Async-Finish Parallelism.

Jonathan K. Lee, Jens Palsberg, Rupak Majumdar, Hong Hong.
SAS 2012.

Lecture Notes on Software Model Checking.

Rupak Majumdar.
Software Safety and Security 2012.

Ideal Abstractions for Well-Structured Transition Systems.

Damien Zufferey, Thomas Wies, Thomas A. Henzinger.
VMCAI 2012.

The Marriage of Exploration and Deduction.

Rupak Majumdar.
VSTTE 2012.

Small Strategies for Safety Games.

Daniel Neider.
ATVA 2011.

Bug-Assist: Assisting Fault Localization in ANSI-C Programs.

Manu Jose, Rupak Majumdar.
CAV 2011.

HMC: Verifying Functional Programs Using Abstract Interpreters.

Ranjit Jhala, Rupak Majumdar, Andrey Rybalchenko.
CAV 2011.

A Lyapunov approach in incremental stability.

Majid Zamani, Rupak Majumdar.
CDC-ECE 2011.

Concurrent Separation Logic and Operational Semantics.

Viktor Vafeiadis.
Electr. Notes Theor. Comput. Sci. 2011.

Preface.

Michael W. Mislove, Joël Ouaknine.
Electr. Notes Theor. Comput. Sci. 2011.

Performance-aware scheduler synthesis for control systems.

Rupak Majumdar, Indranil Saha, Majid Zamani.
EMSOFT 2011.

Test-driven development of concurrent programs using concuerror.

Alkis Gotovos, Maria Christakis, Konstantinos Sagonas.
Erlang Workshop 2011.

End-to-End Guarantees in Embedded Control Systems - (Abstract).

Rupak Majumdar.
Ershov Memorial Conference 2011.

Scheduling large jobs by abstraction refinement.

Thomas A. Henzinger, Vasu Singh, Thomas Wies, Damien Zufferey.
EuroSys 2011.

Minimum Attention Controller Synthesis for Omega-Regular Objectives.

Krishnendu Chatterjee, Rupak Majumdar.
FORMATS 2011.

Static Scheduling in Clouds.

Thomas A. Henzinger, Anmol V. Singh, Vasu Singh, Thomas Wies, Damien Zufferey.
HotCloud 2011.

Pessoa 2.0: a controller synthesis tool for cyber-physical systems.

Pritam Roy, Paulo Tabuada, Rupak Majumdar.
HSCC 2011.

Robust discrete synthesis against unspecified disturbances.

Rupak Majumdar, Elaine Render, Paulo Tabuada.
HSCC 2011.

On the Capabilities of Grammars, Automata, and Transducers Controlled by Monoids.

Georg Zetzsche.
ICALP 2011.

How to make ad hoc proof automation less ad hoc.

Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer.
ICFP 2011.

VCG with Communities on Random Ad Hoc Networks.

Gunes Ercal, Rafit Izhak-Ratzin, Rupak Majumdar, Adam Meyerson.
IJDSN 2011.

Non-parametric parametricity.

Georg Neis, Derek Dreyer, Andreas Rossberg.
J. Funct. Program. 2011.

Separation Logic in the Presence of Garbage Collection.

Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis.
LICS 2011.

Logical Step-Indexed Logical Relations

Derek Dreyer, Amal Ahmed, Lars Birkedal.
Logical Methods in Computer Science 2011.

Trustworthy Numerical Computation in Scala

Eva Darulova, Viktor Kuncak.
OOPSLA 2011.

Detection of Asynchronous Message Passing Errors Using Static Analysis.

Maria Christakis, Konstantinos Sagonas.
PADL 2011.

Cause clue clauses: error localization using maximum satisfiability.

Manu Jose, Rupak Majumdar.
PLDI 2011.

A kripke logical relation between ML and assembly.

Chung-Kil Hur, Derek Dreyer.
POPL 2011.

Relaxed-memory concurrency and verified compilation.

Jaroslav Sevcík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell.
POPL 2011.

Verifying Fence Elimination Optimisations.

Viktor Vafeiadis, Francesco Zappa Nardelli.
SAS 2011.

Behavior-Level Observability Analysis for Operation Gating in Low-Power Behavioral Synthesis.

Jason Cong, Bin Liu, Rupak Majumdar, Zhiru Zhang.
ACM Trans. Design Autom. Electr. Syst. 2010.

Fault-tolerant resynthesis with dual-output LUTs.

Ju-Yueh Lee, Yu Hu, Rupak Majumdar, Lei He, Minming Li.
ASP-DAC 2010.

Automatically Proving Linearizability.

Viktor Vafeiadis.
CAV 2010.

Bounded Underapproximations.

Pierre Ganty, Rupak Majumdar, Benjamin Monmege.
CAV 2010.

libalf: The Automata Learning Framework.

Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker, Daniel Neider, David R. Piegdon.
CAV 2010.

Model Checking of Linearizability of Concurrent List Implementations.

Pavol Cerný, Arjun Radhakrishna, Damien Zufferey, Swarat Chaudhuri, Rajeev Alur.
CAV 2010.

Reachability Games on Automatic Graphs.

Daniel Neider.
CIAA 2010.

Paul Ammann and Jeff Offutt Introduction to Software Testing . Cambridge University Press(2008). ISBN: 978-0-521-88038-1, 322 pp. Hardcover.

Rupak Majumdar.
Comput. J. 2010.

Rewiring for robustness.

Manu Jose, Yu Hu, Rupak Majumdar, Lei He.
DAC 2010.

RALF: Reliability Analysis for Logic Faults - An exact algorithm and its applications.

Samuel B. Luckenbill, Ju-Yueh Lee, Yu Hu, Rupak Majumdar, Lei He.
DATE 2010.

Concurrent Abstract Predicates.

Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, Viktor Vafeiadis.
ECOOP 2010.

A marketplace for cloud resources.

Thomas A. Henzinger, Anmol V. Singh, Vasu Singh, Thomas Wies, Damien Zufferey.
EMSOFT 2010.

Automatic verification of control system implementations.

Adolfo Anta Martinez, Rupak Majumdar, Indranil Saha, Paulo Tabuada.
EMSOFT 2010.

Shape Refinement through Explicit Heap Analysis.

Dirk Beyer, Thomas A. Henzinger, Grégory Théoduloz, Damien Zufferey.
FASE 2010.

Forward Analysis of Depth-Bounded Processes.

Thomas Wies, Damien Zufferey, Thomas A. Henzinger.
FOSSACS 2010.

Discounting in Games across Time Scales

Krishnendu Chatterjee, Rupak Majumdar.
GANDALF 2010.

Towards a Theory of Time-Bounded Verification.

Joël Ouaknine, James Worrell.
ICALP 2010.

On power and fault-tolerance optimization in FPGA physical synthesis.

Manu Jose, Yu Hu, Rupak Majumdar.
ICCAD 2010.

The impact of higher-order state and control effects on local relational reasoning.

Derek Dreyer, Georg Neis, Lars Birkedal.
ICFP 2010.

FlexPRICE: Flexible Provisioning of Resources in a Cloud Environment.

Thomas A. Henzinger, Anmol V. Singh, Vasu Singh, Thomas Wies, Damien Zufferey.
IEEE CLOUD 2010.

Algorithms for Game Metrics (Full Version)

Krishnendu Chatterjee, Luca de Alfaro, Rupak Majumdar, Vishwanath Raman.
Logical Methods in Computer Science 2010.

Systematic testing for control applications.

Rupak Majumdar, Indranil Saha, Zilong Wang.
MEMOCODE 2010.

Static Detection of Race Conditions in Erlang.

Maria Christakis, Konstantinos Sagonas.
PADL 2010.

Parameterized verification of transactional memories.

Michael Emmi, Rupak Majumdar, Roman Manevich.
PLDI 2010.

A relational modal logic for higher-order stateful ADTs.

Derek Dreyer, Georg Neis, Andreas Rossberg, Lars Birkedal.
POPL 2010.

Structuring the verification of heap-manipulating programs.

Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine.
POPL 2010.

On Process-Algebraic Extensions of Metric Temporal Logic.

Christoph Haase, Joël Ouaknine, James Worrell.
Reflections on the Work of C. A. R. Hoare 2010.

F-ing modules.

Andreas Rossberg, Claudio V. Russo, Derek Dreyer.
TLDI 2010.

RGSep Action Inference.

Viktor Vafeiadis.
VMCAI 2010.

Shape Analysis with Reference Set Relations.

Mark Marron, Rupak Majumdar, Darko Stefanovic, Deepak Kapur.
VMCAI 2010.

Software model checking.

Ranjit Jhala, Rupak Majumdar.
ACM Comput. Surv. 2009.

Bi-abductive Resource Invariant Synthesis.

Cristiano Calcagno, Dino Distefano, Viktor Vafeiadis.
APLAS 2009.

Reducing Test Inputs Using Information Partitions.

Rupak Majumdar, Ru-Gang Xu.
CAV 2009.

Fine-Grained Access Control with Object-Sensitive Roles.

Jeffrey Fischer, Daniel Marino, Rupak Majumdar, Todd D. Millstein.
ECOOP 2009.

Deny-Guarantee Reasoning.

Mike Dodds, Xinyu Feng, Matthew J. Parkinson, Viktor Vafeiadis.
ESOP 2009.

Finding heap-bounds for hardware synthesis.

Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jirí Simsa, Satnam Singh, Viktor Vafeiadis.
FMCAD 2009.

Analyzing Real-Time Event-Driven Programs.

Pierre Ganty, Rupak Majumdar.
FORMATS 2009.

Multiset Pushdown Automata.

Manfred Kudlek, Patrick Totzke, Georg Zetzsche.
Fundam. Inform. 2009.

Properties of Multiset Language Classes Defined by Multiset Pushdown Automata.

Manfred Kudlek, Patrick Totzke, Georg Zetzsche.
Fundam. Inform. 2009.

IPR: In-Place Reconfiguration for FPGA fault tolerance.

Zhe Feng, Yu Hu, Lei He, Rupak Majumdar.
ICCAD 2009.

Team Incentives in BitTorrent Systems.

Rafit Izhak-Ratzin, Nikitas Liogkas, Rupak Majumdar.
ICCCN 2009.

Non-parametric parametricity.

Georg Neis, Derek Dreyer, Andreas Rossberg.
ICFP 2009.

Lernverfahren für Automaten über linearisierten XML-Dokumenten.

Daniel Neider.
Informatik Spektrum 2009.

Simultaneous test pattern compaction, ordering and X-filling for testing power reduction.

Ju-Yueh Lee, Yu Hu, Rupak Majumdar, Lei He.
ISQED 2009.

Logical Step-Indexed Logical Relations.

Derek Dreyer, Amal Ahmed, Lars Birkedal.
LICS 2009.

Proving that non-blocking algorithms don't block.

Alexey Gotsman, Byron Cook, Matthew J. Parkinson, Viktor Vafeiadis.
POPL 2009.

State-dependent representation independence.

Amal Ahmed, Derek Dreyer, Andreas Rossberg.
POPL 2009.

Verifying liveness for asynchronous programs.

Pierre Ganty, Rupak Majumdar, Andrey Rybalchenko.
POPL 2009.

Symbolic Robustness Analysis.

Rupak Majumdar, Indranil Saha.
RTSS 2009.

From Tests to Proofs.

Ashutosh Gupta, Rupak Majumdar, Andrey Rybalchenko.
TACAS 2009.

Verifying Reference Counting Implementations.

Michael Emmi, Ranjit Jhala, Eddie Kohler, Rupak Majumdar.
TACAS 2009.

Shape-Value Abstraction for Verifying Linearizability.

Viktor Vafeiadis.
VMCAI 2009.

The Complexity of Coverage.

Krishnendu Chatterjee, Luca de Alfaro, Rupak Majumdar.
APLAS 2008.

The Consistency of Web Conversations.

Jeffrey Fischer, Rupak Majumdar, Francesco Sorrentino.
ASE 2008.

CSIsat: Interpolation for LA+EUF.

Dirk Beyer, Damien Zufferey, Rupak Majumdar.
CAV 2008.

FPGA area reduction by multi-output function based sequential resynthesis.

Yu Hu, Victor Shih, Rupak Majumdar, Lei He.
DAC 2008.

Algorithms for Game Metrics.

Krishnendu Chatterjee, Luca de Alfaro, Rupak Majumdar, Vishwanath Raman.
FSTTCS 2008.

Language Classes Defined by Concurrent Finite Automata.

Matthias Jantzen, Manfred Kudlek, Georg Zetzsche.
Fundam. Inform. 2008.

Nets with Tokens which Carry Data.

Ranko Lazic, Thomas Christopher Newcomb, Joël Ouaknine, A. W. Roscoe, James Worrell.
Fundam. Inform. 2008.

Petri Net Controlled Finite Automata.

Berndt Farwer, Matthias Jantzen, Manfred Kudlek, Heiko Rölke, Georg Zetzsche.
Fundam. Inform. 2008.

Controller Synthesis with Budget Constraints.

Krishnendu Chatterjee, Rupak Majumdar, Thomas A. Henzinger.
HSCC 2008.

Robust FPGA resynthesis based on fault-tolerant Boolean matching.

Yu Hu, Zhe Feng, Lei He, Rupak Majumdar.
ICCAD 2008.

Mixin' up the ML module system.

Derek Dreyer, Andreas Rossberg.
ICFP 2008.

A Theory of Role Composition.

Jeffrey Fischer, Rupak Majumdar.
ICWS 2008.

Exploiting Symmetries to Speed Up SAT-Based Boolean Matching for Logic Synthesis of FPGAs.

Yu Hu, Victor Shih, Rupak Majumdar, Lei He.
IEEE Trans. on CAD of Integrated Circuits and Systems 2008.

Stochastic limit-average games are in EXPTIME.

Krishnendu Chatterjee, Rupak Majumdar, Thomas A. Henzinger.
Int. J. Game Theory 2008.

Testing for buffer overflows with length abstraction.

Ru-Gang Xu, Patrice Godefroid, Rupak Majumdar.
ISSTA 2008.

Game Refinement Relations and Metrics.

Luca de Alfaro, Rupak Majumdar, Vishwanath Raman, Mariëlle Stoelinga.
Logical Methods in Computer Science 2008.

Modular fine-grained concurrency verification.

Viktor Vafeiadis.
Modular fine-grained concurrency verification. 2008.

Labeled Step Sequences in Petri Nets.

Matthias Jantzen, Georg Zetzsche.
Petri Nets 2008.

Proving non-termination.

Ashutosh Gupta, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko, Ru-Gang Xu.
POPL 2008.

Frugal Routing on Wireless Ad-Hoc Networks.

Gunes Ercal, Rafit Izhak-Ratzin, Rupak Majumdar, Adam Meyerson.
SAGT 2008.

Directed test generation using symbolic grammars.

Rupak Majumdar, Ru-Gang Xu.
ASE 2007.

Ensuring consistency in long running transactions.

Jeffrey Fischer, Rupak Majumdar.
ASE 2007.

A Marriage of Rely/Guarantee and Separation Logic.

Viktor Vafeiadis, Matthew J. Parkinson.
CONCUR 2007.

Directed test generation using symbolic grammars.

Rupak Majumdar, Ru-Gang Xu.
ESEC/SIGSOFT FSE 2007.

Exploiting symmetry in SAT-based Boolean matching for heterogeneous FPGA technology mapping.

Yu Hu, Victor Shih, Rupak Majumdar, Lei He.
ICCAD 2007.

Hybrid Concolic Testing.

Rupak Majumdar, Koushik Sen.
ICSE 2007.

Dynamic test input generation for database applications.

Michael Emmi, Rupak Majumdar, Koushik Sen.
ISSTA 2007.

Acute: High-level programming language design for distributed computation.

Peter Sewell, James J. Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair Allen-Williams, Pierre Habouzit, Viktor Vafeiadis.
J. Funct. Program. 2007.

Game Relations and Metrics.

Luca de Alfaro, Rupak Majumdar, Vishwanath Raman, Mariëlle Stoelinga.
LICS 2007.

Tasks: language support for event-driven programming.

Jeffrey Fischer, Rupak Majumdar, Todd D. Millstein.
PEPM 2007.

Path invariants.

Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko.
PLDI 2007.

Interprocedural analysis of asynchronous programs.

Ranjit Jhala, Rupak Majumdar.
POPL 2007.

Lock allocation.

Michael Emmi, Jeffrey S. Fischer, Ranjit Jhala, Rupak Majumdar.
POPL 2007.

Modular Safety Checking for Fine-Grained Concurrency.

Cristiano Calcagno, Matthew J. Parkinson, Viktor Vafeiadis.
SAS 2007.

The software model checker Blast.

Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar.
STTT 2007.

State of the Union: Type Inference Via Craig Interpolation.

Ranjit Jhala, Rupak Majumdar, Ru-Gang Xu.
TACAS 2007.

Invariant Synthesis for Combined Theories.

Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko.
VMCAI 2007.

Verifying Compensating Transactions.

Michael Emmi, Rupak Majumdar.
VMCAI 2007.

Decision Problems for the Verification of Real-Time Software.

Michael Emmi, Rupak Majumdar.
HSCC 2006.

Sudoku as a SAT Problem.

Inês Lynce, Joël Ouaknine.
ISAIM 2006.

Proving correctness of highly-concurrent linearisable objects.

Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, Marc Shapiro.
PPOPP 2006.

Compositional Quantitative Reasoning.

Krishnendu Chatterjee, Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, Mariëlle Stoelinga.
QEST 2006.

Structural Invariants.

Ranjit Jhala, Rupak Majumdar, Ru-Gang Xu.
SAS 2006.

Bit level types for high level reasoning.

Ranjit Jhala, Rupak Majumdar.
SIGSOFT FSE 2006.

Interpolation for data structures.

Deepak Kapur, Rupak Majumdar, Calogero G. Zarba.
SIGSOFT FSE 2006.

Markov Decision Processes with Multiple Objectives.

Krishnendu Chatterjee, Rupak Majumdar, Thomas A. Henzinger.
STACS 2006.

On the universal and existential fragments of the mu -calculus.

Thomas A. Henzinger, Orna Kupferman, Rupak Majumdar.
Theor. Comput. Sci. 2006.

A classification of symbolic transition systems.

Thomas A. Henzinger, Rupak Majumdar, Jean-François Raskin.
ACM Trans. Comput. Log. 2005.

Verifying Quantitative Properties Using Bound Functions.

Arindam Chakrabarti, Krishnendu Chatterjee, Thomas A. Henzinger, Orna Kupferman, Rupak Majumdar.
CHARME 2005.

Code aware resource management.

Luca de Alfaro, Vishwanath Raman, Marco Faella, Rupak Majumdar.
EMSOFT 2005.

Joining dataflow with predicates.

Jeffrey Fischer, Ranjit Jhala, Rupak Majumdar.
ESEC/SIGSOFT FSE 2005.

Permissive interfaces.

Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar.
ESEC/SIGSOFT FSE 2005.

Checking Memory Safety with Blast.

Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar.
FASE 2005.

Quantifying Similarities Between Timed Systems.

Thomas A. Henzinger, Rupak Majumdar, Vinayak S. Prabhu.
FORMATS 2005.

Acute: high-level programming language design for distributed computation.

Peter Sewell, James J. Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair Allen-Williams, Pierre Habouzit, Viktor Vafeiadis.
ICFP 2005.

Path slicing.

Ranjit Jhala, Rupak Majumdar.
PLDI 2005.

Verification of Reactive Systems: Formal Methods and Algorithms. By Klaus Schneider. Springer, Texts in Theoretical Computer Science Series, 2004, ISBN: 3-540-00296-0, pp 600.

Joël Ouaknine.
Softw. Test., Verif. Reliab. 2005.