Papers archive | Programming Languages & Verification

Advice-Guided Reinforcement Learning in a non-Markovian Environment.

Daniel Neider, Jean-Raphaël Gaglione, Ivan Gavran, Ufuk Topcu, Bo Wu, Zhe Xu.
AAAI 2021.

Choosing the Initial State for Online Replanning.

Maximilian Fickert, Ivan Gavran, Ivan Fedotov, Jörg Hoffmann, Rupak Majumdar, Wheeler Ruml.
AAAI 2021.

Responsibility Attribution in Parameterized Markovian Models.

Christel Baier, Florian Funke, Rupak Majumdar.
AAAI 2021.

Robustly Safe Compilation, an Efficient Form of Secure Compilation.

Marco Patrignani, Deepak Garg.
ACM TOPLAS 2021.

VSync: push-button verification and optimization for synchronization primitives on weak memory models.

Jonas Oberhauser, Rafael Lourenco de Lima Chehab, Diogo Behrens, Ming Fu, Antonio Paolillo, Lilith Oberhauser, Koustubha Bhat, Yuzhong Wen, Haibo Chen, Jaeho Kim, Viktor Vafeiadis.
ASPLOS 2021.

Automated Safety Verification of Programs Invoking Neural Networks.

Maria Christakis, Hasan Ferit Eniser, Holger Hermanns, Jörg Hoffmann, Yugesh Kothari, Jianlin Li, Jorge A. Navas, Valentin Wüstholz.
CAV 2021.

Automatically Tailoring Abstract Interpretation to Custom Usage Scenarios.

Muhammad Numair Mansur, Benjamin Mariano, Maria Christakis, Jorge A. Navas, Valentin Wüstholz.
CAV 2021.

GenMC: A Model Checker for Weak Memory Models.

Michalis Kokologiannakis, Viktor Vafeiadis.
CAV 2021.

Porous Invariants.

Engel Lefaucheux, Joël Ouaknine, David Purser, James Worrell.
CAV 2021.

Active Finite Reward Automaton Inference and Reinforcement Learning Using Queries and Counterexamples.

Zhe Xu, Bo Wu, Aditya Ojha, Daniel Neider, Ufuk Topcu.
CD-MAKE 2021.

Safe systems programming in Rust.

Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer.
Commun. ACM 2021.

Generalising Projection in Asynchronous Multiparty Session Types.

Rupak Majumdar, Madhavan Mukund, Felix Stutz, Damien Zufferey.
CONCUR 2021.

Scope-Bounded Reachability in Valence Systems.

Aneesh K. Shetty, Shankara Narayanan Krishna, Georg Zetzsche.
CONCUR 2021.

The Orbit Problem for Parametric Linear Dynamical Systems.

Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Florian Luca, Joël Ouaknine, David Purser, Markus A. Whiteland, James Worrell.
CONCUR 2021.

Lassie: HOL4 tactics by example.

Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, Rupak Majumdar.
CPP 2021.

Metamorphic testing of Datalog engines.

Muhammad Numair Mansur, Maria Christakis, Valentin Wüstholz.
ESEC/SIGSOFT FSE 2021.

The Decidability of Verification under PS 2.0.

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Adwait Godbole, Shankara Narayanan Krishna, Viktor Vafeiadis.
ESOP 2021.

Paracosm: A Test Framework for Autonomous Driving Simulations.

Rupak Majumdar, Aman Shankar Mathur, Marcus Pirron, Laura Stegner, Damien Zufferey.
FASE 2021.

Adaptive strategies for rLTL games.

Satya Prakash Nayak, Daniel Neider, Martin Zimmermann.
HSCC 2021.

The computability of LQR and LQG control.

Rupak Majumdar, Sadegh Soudjani.
HSCC 2021.

Decision Problems for Second-Order Holonomic Recurrences.

Eike Neumann, Joël Ouaknine, James Worrell.
ICALP 2021.

From Verification to Causality-Based Explications (Invited Talk).

Christel Baier, Clemens Dubslaff, Florian Funke, Simon Jantsch, Rupak Majumdar, Jakob Piribauer, Robin Ziemek.
ICALP 2021.

Symbolic reach-avoid control of multi-agent systems.

Rupak Majumdar, Kaushik Mallik, Mahmoud Salamati, Sadegh Soudjani, Mehrdad Zareian.
ICCPS 2021.

GhostCell: separating permissions from data in Rust.

Joshua Yanovski, Hoang-Hai Dang, Ralf Jung, Derek Dreyer.
ICFP 2021.

Higher-order probabilistic adversarial computations: categorical semantics and program logics.

Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Shin-ya Katsumata, Tetsuya Sato.
ICFP 2021.

Verifying Asymptotic Temporal Properties of Continuous-State Probabilistic Systems.

Natsuki Urabe, Rupak Majumdar.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 2021.

A Game-Theoretic Account of Responsibility Allocation.

Christel Baier, Florian Funke, Rupak Majumdar.
IJCAI 2021.

Preface.

Mikolaj Bojanczyk, Thomas Brihaye, Christoph Haase, Slawomir Lasota, Joël Ouaknine, Igor Potapov.
Inf. Comput. 2021.

The emptiness problem for valence automata over graph monoids.

Georg Zetzsche.
Inf. Comput. 2021.

Interval constraint-based mutation testing of numerical specifications.

Clothilde Jeangoudoux, Eva Darulova, Christoph Quirin Lauter.
ISSTA 2021.

Universal Skolem Sets.

Florian Luca, Joël Ouaknine, James Worrell.
LICS 2021.

Holonomic Techniques, Periods, and Decision Problems (Invited Talk).

Joël Ouaknine.
MFCS 2021.

On Positivity and Minimality for Second-Order Holonomic Sequences.

George Kenison, Oleksiy Klurman, Engel Lefaucheux, Florian Luca, Pieter Moree, Joël Ouaknine, Markus A. Whiteland, James Worrell.
MFCS 2021.

On the Complexity of the Escape Problem for Linear Dynamical Systems over Compact Semialgebraic Sets.

Julian D'Costa, Engel Lefaucheux, Eike Neumann, Joël Ouaknine, James Worrell.
MFCS 2021.

The Pseudo-Skolem Problem is Decidable.

Julian D'Costa, Toghrul Karimov, Rupak Majumdar, Joël Ouaknine, Mahmoud Salamati, Sadegh Soudjani, James Worrell.
MFCS 2021.

RefinedC: automating the foundational verification of C code with refined ownership types.

Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, Deepak Garg.
PLDI 2021.

Transfinite Iris: resolving an existential dilemma of step-indexed separation logic.

Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, Lars Birkedal.
PLDI 2021.

A unifying type-theory for higher-order (amortized) cost analysis.

Vineet Rajani, Marco Gaboardi, Deepak Garg, Jan Hoffmann.
POPL 2021.

Context-bounded verification of liveness properties for multithreaded shared-memory programs.

Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche.
POPL 2021.

Deciding ω-regular properties on linear recurrence sequences.

Shaull Almagor, Toghrul Karimov, Edon Kelmendi, Joël Ouaknine, James Worrell.
POPL 2021.

PerSeVerE: persistency semantics for verification under ext4.

Michalis Kokologiannakis, Ilya Kaysin, Azalea Raad, Viktor Vafeiadis.
POPL 2021.

Transfinite step-indexing for termination.

Simon Spies, Neel Krishnaswami, Derek Dreyer.
POPL 2021.

A Characterization of Wreath Products Where Knapsack Is Decidable.

Pascal Bergsträßer, Moses Ganardi, Georg Zetzsche.
STACS 2021.

A Two-Phase Approach for Conditional Floating-Point Verification.

Debasmita Lohar, Clothilde Jeangoudoux, Joshua Sobel, Eva Darulova, Maria Christakis.
TACAS 2021.

Deductive Verification of Floating-Point Java Programs in KeY.

Rosa Abbasi, Jonas Schiffl, Eva Darulova, Mattias Ulbrich, Wolfgang Ahrendt.
TACAS 2021.

General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond.

Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche.
TACAS 2021.

First-Order Orbit Queries.

Shaull Almagor, Joël Ouaknine, James Worrell.
Theory Comput. Syst. 2021.

A type-theory for higher-order amortized cost analysis

Vineet Rajani, Marco Gaboardi, Deepak Garg, Jan Hoffmann.
Technical Report MPI-SWS-2020-004 2020.

PhD thesis: A type-theory for higher-order amortized analysis

Vineet Rajani.
Technical Report MPI-SWS-2020-001 2020.

Exploiting Errors for Efficiency: A Survey from Circuits to Applications.

Phillip Stanley-Marbell, Armin Alaghi, Michael Carbin, Eva Darulova, Lara Dolecek, Andreas Gerstlauer, Ghayoor Gillani, Djordje Jevdjic, Thierry Moreau, Mattia Cacciotti, Alexandros Daglis, Natalie D. Enright Jerger, Babak Falsafi, Sasa Misailovic, Adrian Sampson, Damien Zufferey.
ACM Comput. Surv. 2020.

A Lyapunov Approach for Time-Bounded Reachability of CTMCs and CTMDPs.

Mahmoud Salamati, Sadegh Soudjani, Rupak Majumdar.
ACM Trans. Model. Perform. Evaluation Comput. Syst. 2020.

Synthesizing optimally resilient controllers.

Daniel Neider, Alexander Weinert, Martin Zimmermann.
Acta Informatica 2020.

Parameterized Synthesis with Safety Properties.

Oliver Markgraf, Chih-Duo Hong, Anthony W. Lin, Muhammad Najib, Daniel Neider.
APLAS 2020.

HMC: Model Checking for Hardware Memory Models.

Michalis Kokologiannakis, Viktor Vafeiadis.
ASPLOS 2020.

Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic.

Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter W. O'Hearn, Jules Villard.
CAV 2020.

Interactive Programming for Parametric CAD.

Aman Shankar Mathur, Marcus Pirron, Damien Zufferey.
Comput. Graph. Forum 2020.

Algebraic Invariants for Linear Hybrid Automata.

Rupak Majumdar, Joël Ouaknine, Amaury Pouly, James Worrell.
CONCUR 2020.

On Ranking Function Synthesis and Termination for Polynomial Programs.

Eike Neumann, Joël Ouaknine, James Worrell.
CONCUR 2020.

On the relation between reactive synthesis and supervisory control of non-terminating processes.

Anne-Kathrin Schmuck, Thomas Moor, Rupak Majumdar.
Discret. Event Dyn. Syst. 2020.

Quality Guarantees for Autoencoders via Unsupervised Adversarial Attacks.

Benedikt Böing, Rajarshi Roy, Emmanuel Müller, Daniel Neider.
ECML/PKDD 2020.

Reconciling Event Structures with Modern Multiprocessors.

Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, Viktor Vafeiadis.
ECOOP 2020.

DeepSearch: a simple and effective blackbox attack for deep neural networks.

Fuyuan Zhang, Sankalan Pal Chowdhury, Maria Christakis.
ESEC/SIGSOFT FSE 2020.

Detecting critical bugs in SMT solvers using blackbox mutational fuzzing.

Muhammad Numair Mansur, Maria Christakis, Valentin Wüstholz, Fuyuan Zhang.
ESEC/SIGSOFT FSE 2020.

Harvey: a greybox fuzzer for smart contracts.

Valentin Wüstholz, Maria Christakis.
ESEC/SIGSOFT FSE 2020.

Trace-Relating Compiler Correctness and Secure Compilation.

Carmine Abate, Roberto Blanco, Stefan Ciobaca, Adrien Durier, Deepak Garg, Catalin Hritcu, Marco Patrignani, Éric Tanter, Jérémy Thibault.
ESOP 2020.

Learning Properties in LTL ∩ ACTL from Positive Examples Only.

Rüdiger Ehlers, Ivan Gavran, Daniel Neider.
FMCAD 2020.

Holonomic Techniques, Periods, and Decision Problems (Invited Talk).

Joël Ouaknine.
FSTTCS 2020.

Reachability in Dynamical Systems with Rounding.

Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, Amaury Pouly, David Purser, Markus A. Whiteland.
FSTTCS 2020.

From LTL to rLTL monitoring: improved monitorability through robust semantics.

Corto Mascle, Daniel Neider, Maximilian Schwenger, Paulo Tabuada, Alexander Weinert, Martin Zimmermann.
HSCC 2020.

On abstraction-based controller design with output feedback.

Rupak Majumdar, Necmiye Ozay, Anne-Kathrin Schmuck.
HSCC 2020.

Symbolic controller synthesis for Büchi specifications on stochastic systems.

Rupak Majumdar, Kaushik Mallik, Sadegh Soudjani.
HSCC 2020.

Invariants for Continuous Linear Dynamical Systems.

Shaull Almagor, Edon Kelmendi, Joël Ouaknine, James Worrell.
ICALP 2020.

On Decidability of Time-Bounded Reachability in CTMDPs.

Rupak Majumdar, Mahmoud Salamati, Sadegh Soudjani.
ICALP 2020.

Rational Subsets of Baumslag-Solitar Groups.

Michaël Cadilhac, Dmitry Chistikov, Georg Zetzsche.
ICALP 2020.

The Complexity of Bounded Context Switching with Dynamic Thread Creation.

Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche.
ICALP 2020.

The Complexity of Knapsack Problems in Wreath Products.

Michael Figelius, Moses Ganardi, Markus Lohrey, Georg Zetzsche.
ICALP 2020.

Joint Inference of Reward Machines and Policies for Reinforcement Learning.

Zhe Xu, Ivan Gavran, Yousef Ahmad, Rupak Majumdar, Daniel Neider, Ufuk Topcu, Bo Wu.
ICAPS 2020.

DeepEquaL: Deep Learning Based Mathematical Equation to Latex Generation.

Ghaith Bilbeisi, Sheraz Ahmed, Rupak Majumdar.
ICONIP 2020.

Targeted greybox fuzzing with static lookahead analysis.

Valentin Wüstholz, Maria Christakis.
ICSE 2020.

Automated Controller and Sensor Configuration Synthesis Using Dimensional Analysis.

Marcus Pirron, Damien Zufferey, Phillip Stanley-Marbell.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 2020.

Learning Interpretable Models in the Property Specification Language.

Rajarshi Roy, Dana Fisman, Daniel Neider.
IJCAI 2020.

On the skolem problem and prime powers.

George Kenison, Richard Lipton, Joël Ouaknine, James Worrell.
ISSAC 2020.

A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification Engines.

Daniel Neider, P. Madhusudan, Shambwaditya Saha, Pranav Garg, Daejun Park.
J. Autom. Reason. 2020.

An Approach to Regular Separability in Vector Addition Systems.

Wojciech Czerwinski, Georg Zetzsche.
LICS 2020.

Extensions of ω-Regular Languages.

Mikolaj Bojanczyk, Edon Kelmendi, Rafal Stefanski, Georg Zetzsche.
LICS 2020.

Knapsack and the Power Word Problem in Solvable Baumslag-Solitar Groups.

Markus Lohrey, Georg Zetzsche.
MFCS 2020.

On LTL Model Checking for Low-Dimensional Discrete Linear Dynamical Systems.

Toghrul Karimov, Joël Ouaknine, James Worrell.
MFCS 2020.

Optimally Resilient Strategies in Pushdown Safety Games.

Daniel Neider, Patrick Totzke, Martin Zimmermann.
MFCS 2020.

Interactive synthesis of temporal specifications from examples and natural language.

Ivan Gavran, Eva Darulova, Rupak Majumdar.
OOPSLA 2020.

Multiparty motion coordination: from choreographies to robotics programs.

Rupak Majumdar, Nobuko Yoshida, Damien Zufferey.
OOPSLA 2020.

Perfectly parallel fairness certification of neural networks.

Caterina Urban, Maria Christakis, Valentin Wüstholz, Fuyuan Zhang.
OOPSLA 2020.

Persistent Owicki-Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86.

Azalea Raad, Ori Lahav, Viktor Vafeiadis.
OOPSLA 2020.

Programming at the edge of synchrony.

Cezara Dragoi, Josef Widder, Damien Zufferey.
OOPSLA 2020.

Testing consensus implementations using communication closure.

Cezara Dragoi, Constantin Enea, Burcu Kulahcioglu Ozkan, Rupak Majumdar, Filip Niksic.
OOPSLA 2020.

Promising 2.0: global optimizations in relaxed memory concurrency.

Sung-Hwan Lee, Minki Cho, Anton Podkopaev, Soham Chakraborty, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis.
PLDI 2020.

Synthesizing structured CAD models with equality saturation and inverse transformations.

Chandrakana Nandi, Max Willsey, Adam Anderson, James R. Wilcox, Eva Darulova, Dan Grossman, Zachary Tatlock.
PLDI 2020.

Persistency semantics of the Intel-x86 architecture.

Azalea Raad, John Wickerson, Gil Neiger, Viktor Vafeiadis.
POPL 2020.

RustBelt meets relaxed memory.

Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, Derek Dreyer.
POPL 2020.

Stacked borrows: An aliasing model for Rust.

Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, Derek Dreyer.
POPL 2020.

The future is ours: Prophecy variables in separation logic.

Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, Bart Jacobs.
POPL 2020.

The high-level benefits of low-level sandboxing.

Michael Sammler, Deepak Garg, Derek Dreyer, Tadeusz Litak.
POPL 2020.

Counterexample- and Simulation-Guided Floating-Point Loop Invariant Synthesis.

Anastasiia Izycheva, Eva Darulova, Helmut Seidl.
SAS 2020.

How Fast Can You Escape a Compact Polytope?

Julian D'Costa, Engel Lefaucheux, Joël Ouaknine, James Worrell.
STACS 2020.

Lab Conditions for Research on Explainable Automated Decisions.

Christel Baier, Maria Christakis, Timo P. Gros, David Groß, Stefan Gumhold, Holger Hermanns, Jörg Hoffmann, Michaela Klauck.
TAILOR 2020.

Lazy Abstraction-Based Controller Synthesis.

Kyle Hsu, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck.
ATVA 2019.

Synthesizing Efficient Low-Precision Kernels.

Anastasiia Izycheva, Eva Darulova, Helmut Seidl.
ATVA 2019.

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.

Incremental Abstraction Computation for Symbolic Controller Synthesis in a Changing Environment.

Yunjun Bai, Kaushik Mallik, Anne-Kathrin Schmuck, Damien Zufferey, Rupak Majumdar.
CDC 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.

Learning-Based Synthesis of Safety Controllers.

Daniel Neider, Oliver Markgraf.
FMCAD 2019.

Regular Separability and Intersection Emptiness Are Independent Problems.

Ramanathan S. Thinniyam, Georg Zetzsche.
FSTTCS 2019.

Robust, Expressive, and Quantitative Linear Temporal Logics: Pick any Two for Free.

Daniel Neider, Alexander Weinert, Martin Zimmermann.
GandALF 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.

Relational cost analysis for functional-imperative programs.

Weihao Qu, Marco Gaboardi, Deepak Garg.
ICFP 2019.

Compositional Synthesis of Finite-State Abstractions.

Kaushik Mallik, Anne-Kathrin Schmuck, Sadegh Soudjani, Rupak Majumdar.
IEEE Trans. Autom. Control. 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. Autom. Control. 2019.

Sound Probabilistic Numerical Error Analysis.

Debasmita Lohar, Milos Prokop, Eva Darulova.
IFM 2019.

MPERL: Hardware and Software Co-design for Robotic Manipulators ©.

Marcus Pirron, Damien Zufferey.
IROS 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.

A relational logic for higher-order programs.

Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub.
J. Funct. Program. 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.
Log. Methods Comput. Sci. 2019.

Evaluating Branching Heuristics in Interval Constraint Propagation for Satisfiability.

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

Effective lock handling in stateless model checking.

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

Trace aware random testing for distributed systems.

Burcu Kulahcioglu Ozkan, Rupak Majumdar, Simin Oraee.
OOPSLA 2019.

Weak persistency semantics from the ground up: formalising the persistency semantics of ARMv8 and transactional models.

Azalea Raad, John Wickerson, Viktor Vafeiadis.
OOPSLA 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.

On the Monniaux Problem in Abstract Interpretation.

Nathanaël Fijalkow, Engel Lefaucheux, Pierre Ohlmann, Joël Ouaknine, Amaury Pouly, James Worrell.
SAS 2019.

Sorcar: Property-Driven Algorithms for Learning Conjunctive Invariants.

Daniel Neider, Shambwaditya Saha, Pranav Garg, P. Madhusudan.
SAS 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 Informatica 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.

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.

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

Mengda He, Viktor Vafeiadis, Shengchao Qin, João F. Ferreira.
Int. J. Parallel Program. 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.
Log. Methods Comput. Sci. 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.

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

Vineet Rajani, Iulia Bastys, Willard Rafnsson, Deepak Garg.
ACM SIGLOG News 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. Embed. Comput. Syst. 2017.

Testing Cyber-Physical Systems through Bayesian Optimization.

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

Approximate counting in SMT and value estimation for probabilistic programs.

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

Dynamic Bayesian networks for formal verification of structured stochastic processes.

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

Verification of population protocols.

Javier Esparza, Pierre Ganty, Jérôme Leroux, Rupak Majumdar.
Acta Informatica 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.
Discret. Event Dyn. Syst. 2017.

A Characterization for Decidable Separability by Piecewise Testable Languages.

Wojciech Czerwinski, Wim Martens, Lorijn van Rooijen, Marc Zeitoun, Georg Zetzsche.
Discret. Math. Theor. Comput. Sci. 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 Syst. Des. 2017.

Quantifying conformance using the Skorokhod metric.

Jyotirmoy V. Deshmukh, Rupak Majumdar, Vinayak S. Prabhu.
Formal Methods Syst. Des. 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 Inf. Technol. 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.

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.

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.

Knapsack and subset sum problems in nilpotent, polycyclic, and co-context-free groups.

Daniel König, Markus Lohrey, Georg Zetzsche.
AMS-EMS-SPM Joint Meeting 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.
Bull. 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.

Permutations of context-free, ET0L and indexed languages.

Tara Brough, Laura Ciobanu, Murray Elder, Georg Zetzsche.
Discret. Math. Theor. Comput. Sci. 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.

Relating Reachability Problems in Timed and Counter Automata.

Christoph Haase, Joël Ouaknine, James Worrell.
Fundam. Informaticae 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.

On linear recurrence sequences and loop termination.

Joël Ouaknine, James Worrell.
ACM SIGLOG News 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.

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 Syst. Des. 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.
Log. Methods Comput. Sci. 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.

Abstractions from proofs.

Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan.
ACM SIGPLAN Notices 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. Autom. Control. 2014.

Towards Robustness for Cyber-Physical Systems.

Paulo Tabuada, Sina Yamac Caliskan, Matthias Rungger, Rupak Majumdar.
IEEE Trans. Autom. Control. 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. Embed. 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.

Decision Problems for Linear Recurrence Sequences.

Joël Ouaknine.
FCT 2013.

Algorithmic probabilistic game semantics - Playing games with automata.

Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, James Worrell.
Formal Methods Syst. Des. 2013.

Code aware resource management.

Krishnendu Chatterjee, Luca de Alfaro, Marco Faella, Rupak Majumdar, Vishwanath Raman.
Formal Methods Syst. Des. 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.

From tests to proofs.

Ashutosh Gupta, Rupak Majumdar, Andrey Rybalchenko.
Int. J. Softw. Tools Technol. Transf. 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.

A Static Analysis Framework for Livelock Freedom in CSP

Joël Ouaknine, Hristina Palikareva, A. W. Roscoe, James Worrell.
Log. Methods Comput. Sci. 2013.

On the Complexity of Equivalence and Minimisation for Q-weighted Automata

Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, James Worrell.
Log. Methods Comput. Sci. 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.

Backstepping controller synthesis and characterizations of incremental stability.

Majid Zamani, Nathan van de Wouw, Rupak Majumdar.
Syst. Control. Lett. 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.

Automatic predicate abstraction of C programs.

Thomas Ball, Rupak Majumdar, Todd D. Millstein, Sriram K. Rajamani.
ACM SIGPLAN Notices 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 Syst. Des. 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.

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/ECC 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.
Int. J. Distributed Sens. Networks 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.
Log. Methods Comput. Sci. 2011.

Concurrent Separation Logic and Operational Semantics.

Viktor Vafeiadis.
MFPS 2011.

Preface.

Michael W. Mislove, Joël Ouaknine.
MFPS 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.
Log. Methods Comput. Sci. 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.

Faster FDR Counterexample Generation Using SAT-Solving.

Hristina Palikareva, Joël Ouaknine, Bill Roscoe.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 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. Informaticae 2009.

Properties of Multiset Language Classes Defined by Multiset Pushdown Automata.

Manfred Kudlek, Patrick Totzke, Georg Zetzsche.
Fundam. Informaticae 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.
Inform. Spektrum 2009.

An abstraction-based decision procedure for bit-vector arithmetic.

Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady.
Int. J. Softw. Tools Technol. Transf. 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. Informaticae 2008.

Nets with Tokens which Carry Data.

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

Petri Net Controlled Finite Automata.

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

Universality Analysis for One-Clock Timed Automata.

Parosh Aziz Abdulla, Johann Deneux, Joël Ouaknine, Karin Quaas, James Worrell.
Fundam. Informaticae 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. Comput. Aided Des. Integr. Circuits Syst. 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.
Log. Methods Comput. Sci. 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.

The software model checker Blast.

Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar.
Int. J. Softw. Tools Technol. Transf. 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.

On the decidability and complexity of Metric Temporal Logic over finite words.

Joël Ouaknine, James Worrell.
Log. Methods Comput. Sci. 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.

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.

Parallel Assignments in Software Model Checking.

Murray Stokely, Sagar Chaki, Joël Ouaknine.
Electron. Notes Theor. Comput. Sci. 2006.

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.

Concurrent software verification with states, events, and deadlocks.

Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha.
Formal Aspects Comput. 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.

Computational challenges in bounded model checking.

Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman.
Int. J. Softw. Tools Technol. Transf. 2005.

On Timed Models and Full Abstraction.

Gavin Lowe, Joël Ouaknine.
MFPS 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. Verification Reliab. 2005.