Papers archive | Cyber-Physical Systems

Positive Almost-Sure Termination: Complexity and Proof Rules.

Rupak Majumdar, V. R. Sathiyanarayana.
POPL 2024.

Solving Two-Player Games Under Progress Assumptions.

Anne-Kathrin Schmuck, K. S. Thejaswini, Irmak Saglam, Satya Prakash Nayak.
VMCAI 2024.

Synthesizing Permissive Winning Strategy Templates for Parity Games

Ashwani Anand, Satya Prakash Nayak, and Anne-Kathrin Schmuck.
Technical Report MPI-SWS-2023-001 2023.

Markov Decision Processes with Time-Varying Geometric Discounting.

Jiarui Gan, Annika Hennes, Rupak Majumdar, Debmalya Mandal, Goran Radanovic.
AAAI 2023.

Neural Abstraction-Based Controller Synthesis and Deployment.

Rupak Majumdar, Mahmoud Salamati, Sadegh Soudjani.
ACM Trans. Embed. Comput. Syst. 2023.

A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties.

Rupak Majumdar, Kaushik Mallik, Mateusz Rychlicki, Anne-Kathrin Schmuck, Sadegh Soudjani.
CAV 2023.

Making sf IP=sf PSPACE Practical: Efficient Interactive Protocols for BDD Algorithms.

Eszter Couillard, Philipp Czerner, Javier Esparza, Rupak Majumdar.
CAV 2023.

Solving String Constraints Using SAT.

Kevin Lotz, Amit Goel, Bruno Dutertre, Benjamin Kiesl-Reiter, Soonho Kong, Rupak Majumdar, Dirk Nowotka.
CAV 2023.

Synthesizing Permissive Winning Strategy Templates for Parity Games.

Ashwani Anand, Satya Prakash Nayak, Anne-Kathrin Schmuck.
CAV 2023.

Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete.

Shankara Narayanan Krishna, Khushraj Nanik Madnani, Rupak Majumdar, Paritosh K. Pandya.
CONCUR 2023.

Solving Odd-Fair Parity Games.

Irmak Saglam, Anne-Kathrin Schmuck.
FSTTCS 2023.

Lazy Synthesis of Symbolic Output-Feedback Controllers for State-Based Safety Specifications.

Mehrdad Zareian, Anne-Kathrin Schmuck.
HSCC 2023.

Poster Abstract: A Toolchain for Accelerated Symbolic Control.

Rupak Majumdar, Kaushik Mallik, Mateusz Rychlicki, Anne-Kathrin Schmuck, Sadegh Soudjani.
HSCC 2023.

Poster Abstract: Permissiveness for Strategy Adaptation.

Ashwani Anand, Satya Prakash Nayak, Anne-Kathrin Schmuck.
HSCC 2023.

Poster Abstract: Towards Seamless Reactivity of Hybrid Control.

Lucas Neves Egidio, Satya Prakash Nayak, Matteo Della Rossa, Anne-Kathrin Schmuck, Raphaël M. Jungers.
HSCC 2023.

Supervisory Controller Synthesis for Nonterminating Processes Is an Obliging Game.

Rupak Majumdar, Anne-Kathrin Schmuck.
IEEE Trans. Autom. Control. 2023.

G(IP) C: Temporally Isolated Multiprocessor Real-Time IPC with Server-to-Server Invocations.

Cédric Courtaud, Björn B. Brandenburg.
RTAS 2023.

CTA: A Correlation-Tolerant Analysis of the Deadline-Failure Probability of Dependent Tasks.

Filip Markovic, Pierre Roux, Sergey Bozhko, Alessandro V. Papadopoulos, Björn B. Brandenburg.
RTSS 2023.

What Really is pWCET? A Rigorous Axiomatic Proposal.

Sergey Bozhko, Filip Markovic, Georg von der Brüggen, Björn B. Brandenburg.
RTSS 2023.

Computing Adequately Permissive Assumptions for Synthesis.

Ashwani Anand, Kaushik Mallik, Satya Prakash Nayak, Anne-Kathrin Schmuck.
TACAS 2023.

Fast Symbolic Algorithms for Omega-Regular Games under Strong Transition Fairness.

Tamajit Banerjee, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck, Sadegh Soudjani.
TheoretiCS 2023.

Foundational Response-Time Analysis as Explainable Evidence of Timeliness.

Marco Maida, Sergey Bozhko, Björn B. Brandenburg.
ECRTS 2022.

Multiprocessor Real-Time Locking Protocols.

Björn B. Brandenburg.
Handbook of Real-Time Computing 2022.

BOCoSy: Small but Powerful Symbolic Output-Feedback Control.

Bernd Finkbeiner, Kaushik Mallik, Noemi Passing, Malte Schledjewski, Anne-Kathrin Schmuck.
HSCC 2022.

Subcubic certificates for CFL reachability.

Dmitry Chistikov, Rupak Majumdar, Philipp Schepper.
POPL 2022.

Work in Progress: Automatic Response-Time Analysis for Arbitrary Real-Time Linux Workloads.

Marco Perronet, Marco Maida, Cédric Courtaud, Björn B. Brandenburg.
RTAS 2022.

From Intuition to Coq: A Case Study in Verified Response-Time Analysis 1 of FIFO Scheduling.

Kimaya Bedarkar, Mariam Vardishvili, Sergey Bozhko, Marco Maida, Björn B. Brandenburg.
RTSS 2022.

In-ConcReTeS: Interactive Consistency meets Distributed Real-Time Systems, Again!

Arpan Gujarati, Ningfeng Yang, Björn B. Brandenburg.
RTSS 2022.

A Direct Symbolic Algorithm for Solving Stochastic Rabin Games.

Tamajit Banerjee, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck, Sadegh Soudjani.
TACAS 2022.

Pacer: Comprehensive Network Side-Channel Mitigation in the Cloud.

Aastha Mehta, Mohamed Alzayat, Roberta De Viti, Björn B. Brandenburg, Peter Druschel, Deepak Garg.
USENIX Security Symposium 2022.

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.

Symbolic Qualitative Control for Stochastic Systems via Finite Parity Games.

Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck, Sadegh Soudjani.
ADHS 2021.

Generalising Projection in Asynchronous Multiparty Session Types.

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

Paracosm: A Test Framework for Autonomous Driving Simulations.

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

The computability of LQR and LQG control.

Rupak Majumdar, Sadegh Soudjani.
HSCC 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.

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.

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

Anthony W. Lin, Rupak Majumdar.
Log. Methods Comput. Sci. 2021.

Automatic Latency Management for ROS 2: Benefits, Challenges, and Open Problems.

Tobias Blaß, Arne Hamann, Ralph Lange, Dirk Ziegenbein, Björn B. Brandenburg.
RTAS 2021.

A ROS 2 Response-Time Analysis Exploiting Starvation Freedom and Execution-Time Variance.

Tobias Blaß, Daniel Casini, Sergey Bozhko, Björn B. Brandenburg.
rtss 2021.

Efficiently Approximating the Worst-Case Deadline Failure Probability Under EDF.

Georg von der Brüggen, Nico Piatkowski, Kuan-Hsun Chen, Jian-Jia Chen, Katharina Morik, Björn B. Brandenburg.
rtss 2021.

Monte Carlo Response-Time Analysis.

Sergey Bozhko, Georg von der Brüggen, Björn B. Brandenburg.
rtss 2021.

Work-in-Progress: Automatically Generated Response-Time Proofs as Evidence of Timeliness.

Marco Maida, Sergey Bozhko, Björn B. Brandenburg.
rtss 2021.

Abstract Response-Time Analysis: A Formal Foundation for the Busy-Window Principle

Sergey Bozhko, Björn B. Brandenburg.
Technical Report MPI-SWS-2020-003 2020.

Nested, but Separate: Isolating Unrelated Critical Sections in Real-Time Nested Locking

James Robb, Björn B. Brandenburg.
Technical Report MPI-SWS-2020-002 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.

Resilient Abstraction-Based Controller Design.

Stanly Samuel, Kaushik Mallik, Anne-Kathrin Schmuck, Daniel Neider.
CDC 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.

Abstract Response-Time Analysis: A Formal Foundation for the Busy-Window Principle.

Sergey Bozhko, Björn B. Brandenburg.
ECRTS 2020.

Nested, but Separate: Isolating Unrelated Critical Sections in Real-Time Nested Locking.

James Robb, Björn B. Brandenburg.
ECRTS 2020.

On abstraction-based controller design with output feedback.

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

Resilient abstraction-based controller design.

Stanly Samuel, Kaushik Mallik, Anne-Kathrin Schmuck, Daniel Neider.
HSCC 2020.

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

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

On Decidability of Time-Bounded Reachability in CTMDPs.

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

DeepEquaL: Deep Learning Based Mathematical Equation to Latex Generation.

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

Assume-Guarantee Distributed Synthesis.

Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck, Damien Zufferey.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 2020.

Multiparty motion coordination: from choreographies to robotics programs.

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

Testing consensus implementations using communication closure.

Cezara Dragoi, Constantin Enea, Burcu Kulahcioglu Ozkan, Rupak Majumdar, Filip Niksic.
OOPSLA 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.

Real-Time Replica Consistency over Ethernet with Reliability Bounds.

Arpan Gujarati, Sergey Bozhko, Björn B. Brandenburg.
RTAS 2020.

Response-Time Analysis for Non-Preemptive Global Scheduling with FIFO Spin Locks.

Suhail Nogd, Geoffrey Nelissen, Mitra Nasri, Björn B. Brandenburg.
RTSS 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.

An Exact Schedulability Test for Non-Preemptive Self-Suspending Real-Time Tasks.

Beyazit Yalcinkaya, Mitra Nasri, Björn B. Brandenburg.
DATE 2019.

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

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

From Iteration to System Failure: Characterizing the FITness of Periodic Weakly-Hard Systems.

Arpan Gujarati, Mitra Nasri, Rupak Majumdar, Björn B. Brandenburg.
ECRTS 2019.

Response-Time Analysis of Limited-Preemptive Parallel DAG Tasks Under Global Scheduling.

Mitra Nasri, Geoffrey Nelissen, Björn B. Brandenburg.
ECRTS 2019.

Response-Time Analysis of ROS 2 Processing Chains Under Reservation-Based Scheduling.

Daniel Casini, Tobias Blaß, Ingo Lütkebohle, Björn B. Brandenburg.
ECRTS 2019.

Achal: building highly reliable networked control systems.

Arpan Gujarati, Malte Appel, Björn B. Brandenburg.
EMSOFT Companion 2019.

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

Joachim Bard, Heiko Becker, Eva Darulova.
FM 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. 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.

Trace aware random testing for distributed systems.

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

Checking linearizability using hitting families.

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

Correspondence article: a correction of the reduction-based schedulability analysis for APA scheduling.

Arpan Gujarati, Felipe Cerqueira, Björn B. Brandenburg, Geoffrey Nelissen.
Real Time Syst. 2019.

Many suspensions, many problems: a review of self-suspending tasks in real-time systems.

Jian-Jia Chen, Geoffrey Nelissen, Wen-Hung Huang, Maolin Yang, Björn B. Brandenburg, Konstantinos Bletsas, Cong Liu, Pascal Richard, Frédéric Ridouard, Neil C. Audsley, Raj Rajkumar, Dionisio de Niz, Georg von der Brüggen.
Real Time Syst. 2019.

From Code to Weakly Hard Constraints: A Pragmatic End-to-End Toolchain for Timed C.

Saranya Natarajan, Mitra Nasri, David Broman, Björn B. Brandenburg, Geoffrey Nelissen.
RTSS 2019.

Environmentally-Friendly GR(1) Synthesis.

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

Environmentally-friendly GR(1) Synthesis

Rupak Majumdar, Nir Piterman, Anne-Kathrin Schmuck.
Technical Report MPI-SWS-2018-008 2018.

An Exact Schedulability Test for Non-Preemptive Self-Suspending Real-Time Tasks -- Extended Version

Beyazit Yalcinkaya, Mitra Nasri, Bjoern Brandenburg.
Technical Report MPI-SWS-2018-009 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.

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.

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.

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.

A Response-Time Analysis for Non-Preemptive Job Sets under Global Scheduling.

Mitra Nasri, Geoffrey Nelissen, Björn B. Brandenburg.
ECRTS 2018.

On Strong and Weak Sustainability, with an Application to Self-Suspending Real-Time Tasks.

Felipe Cerqueira, Geoffrey Nelissen, Björn B. Brandenburg.
ECRTS 2018.

Quantifying the Resiliency of Fail-Operational Real-Time Networked Control Systems.

Arpan Gujarati, Mitra Nasri, Björn B. Brandenburg.
ECRTS 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.

Tableau: a high-throughput and predictable VM scheduler for high-density workloads.

Manohar Vanga, Arpan Gujarati, Björn B. Brandenburg.
EuroSys 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.

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

Rupak Majumdar.
FSTTCS 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.

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.

Randomized testing of distributed systems with probabilistic guarantees.

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

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

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

FIFO with Offsets: High Schedulability with Low Overheads.

Mitra Nasri, Robert I. Davis, Björn B. Brandenburg.
RTAS 2018.

Scalable Memory Reclamation for Multi-Core, Real-Time Systems.

Yuxin Ren, Guyue Liu, Gabriel Parmer, Björn B. Brandenburg.
RTAS 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.

An Exact and Sustainable Analysis of Non-Preemptive Scheduling

Mitra Nasri and Björn Brandenburg.
RTSS 2017

Supporting low-latency, low-criticality tasks in a certified mixed-criticality OS.

Manohar Vanga, Andrea Bastoni, Henrik Theiling, Björn B. Brandenburg.
RTNS 2017.

Offline Equivalence: A Non-Preemptive Scheduling Technique for Resource-Constrained Embedded Real-Time Systems

Mitra Nasri and Björn Brandenburg.
RTAS 2017.

TimerShield: Protecting High-Priority Tasks from Low-Priority Timer Interference

Pratyush Patel, Manohar Vanga, and Björn Brandenburg.
RTAS 2017.

Master's Thesis: Reactive Controller Synthesis for Mobile Robotics

Adrian Leva.
Technical Report MPI-SWS-2017-001 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.

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.

Dynamic hierarchical reactive controller synthesis.

Anne-Kathrin Schmuck, Rupak Majumdar, Adrian Leva.
Discret. Event Dyn. Syst. 2017.

Synthesis of Solutions for Shaded Area Geometry Problems.

Chris Alvin, Sumit Gulwani, Rupak Majumdar, Supratik Mukhopadhyay.
FLAIRS 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.

A Note on the Period Enforcer Algorithm for Self-Suspending Tasks.

Jian-Jia Chen, Björn B. Brandenburg.
Leibniz Trans. Embed. Syst. 2017.

An Exact and Sustainable Analysis of Non-preemptive Scheduling.

Mitra Nasri, Björn B. Brandenburg.
RTSS 2017.

On Flexible and Robust Parameter Assignment for Periodic Real-Time Components

Mitra Nasri.
9th International Workshop on Compositional Theory and Technology for Real-Time Embedded Systems (CRTS) 2016.

A Blocking Bound for Nested FIFO Spin Locks

Alessandro Biondi, Björn B. Brandenburg, Alexander Wieder.
RTSS 2016.

Global Scheduling Not Required: Simple, Near-Optimal Multiprocessor Real-Time Scheduling with Semi-Partitioned Reservations

Björn B. Brandenburg and Mahircan Gül.
RTSS 2016.

On the Problem of Finding Optimal Harmonic Periods

Morteza Mohaqeqi, Mitra Nasri, Yang Xu, Anton Cervin, Karl-Erik Arzen.
RTNS 2016.

Quantifying the Effect of Period Ratios on Schedulability of Rate Monotonic

Mitra Nasri, Morteza Mohaqeqi, Gerhard Fohler.
RTNS 2016.

Lightweight Real-Time Synchronization under P-EDF on Symmetric and Asymmetric Multiprocessors

Alessandro Biondi, Björn B. Brandenburg.
Technical Report MPI-SWS-2016-003 2016.

Computing Distances between Reach Flowpipes.

Rupak Majumdar, Vinayak S. Prabhu.
HSCC 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.

Symbolic Model Checking for Factored Probabilistic Models.

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

Supervisory control synthesis for deterministic context free specification languages - Enforcing controllability least restrictively.

Anne-Kathrin Schmuck, Sven Schneider, Jörg Raisch, Uwe Nestmann.
Discret. Event Dyn. Syst. 2016.

Lightweight Real-Time Synchronization under P-EDF on Symmetric and Asymmetric Multiprocessors.

Alessandro Biondi, Björn B. Brandenburg.
ECRTS 2016.

Multiprocessor Real-Time Scheduling with Hierarchical Processor Affinities.

Vincenzo Bonifaci, Björn B. Brandenburg, Gianlorenzo D'Angelo, Alberto Marchetti-Spaccamela.
ECRTS 2016.

PROSA: A Case for Readable Mechanized Schedulability Analysis.

Felipe Cerqueira, Felix Stutz, Björn B. Brandenburg.
ECRTS 2016.

Parameterized Verification of Asynchronous Shared-Memory Systems.

Javier Esparza, Pierre Ganty, Rupak Majumdar.
J. ACM 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.

Supervisory controller synthesis for decomposable deterministic context free specification languages.

Kaushik Mallik, Anne-Kathrin Schmuck.
WODES 2016.

Global Real-Time Semaphore Protocols: A Survey, Unified Analysis, and Comparison

Maolin Yang, Alexander Wieder, Björn B. Brandenburg.
Technical Report MPI-SWS-2015-003 2015.

iThreads: A Threading Library for Parallel Incremental Computation.

Pramod Bhatotia, Pedro Fonseca, Umut A. Acar, Björn B. Brandenburg, Rodrigo Rodrigues.
ASPLOS 2015.

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

Rupak Majumdar, Zilong Wang.
CAV 2015.

Comparing asynchronous l-complete approximations and quotient based abstractions.

Anne-Kathrin Schmuck, Paulo Tabuada, Jörg Raisch.
CDC 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.

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.

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

Rayna Dimitrova, Rupak Majumdar.
GandALF 2015.

Computing the Skorokhod distance between polygonal traces.

Rupak Majumdar, Vinayak S. Prabhu.
HSCC 2015.

Dynamic scheduling for networked control systems.

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

Multiprocessor real-time scheduling with arbitrary processor affinities: from practice to theory.

Arpan Gujarati, Felipe Cerqueira, Björn B. Brandenburg.
Real Time Syst. 2015.

Global Real-Time Semaphore Protocols: A Survey, Unified Analysis, and Comparison.

Maolin Yang, Alexander Wieder, Björn B. Brandenburg.
RTSS 2015.

When Is CAN the Weakest Link? A Bound on Failures-in-Time in CAN-Based Real-Time Systems.

Arpan Gujarati, Björn B. Brandenburg.
RTSS 2015.

Approximate Counting in SMT and Value Estimation for Probabilistic Programs.

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

Scaling Global Scheduling with Message Passing

Felipe Cerqueira, Manohar Vanga, Björn B. Brandenburg.
Technical Report MPI-SWS-2014-001 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.

An SMT-Based Approach to Coverability Analysis.

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

Regression Test Selection for Distributed Software Histories.

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

Constructing (Bi)similar finite state abstractions using asynchronous l-complete approximations.

Anne-Kathrin Schmuck, Jörg Raisch.
CDC 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.

The FMLP+: An Asymptotically Optimal Real-Time Locking Protocol for Suspension-Aware Analysis.

Björn B. Brandenburg.
ECRTS 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.

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.

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.

Blocking Optimality in Distributed Real-Time Locking Protocols.

Björn Bernhard Brandenburg.
Leibniz Trans. Embed. Syst. 2014.

Simulation and bisimulation over multiple time scales in a behavioral setting.

Anne-Kathrin Schmuck, Jörg Raisch.
MED 2014.

SKI: Exposing Kernel Concurrency Bugs through Systematic Schedule Exploration.

Pedro Fonseca, Rodrigo Rodrigues, Björn B. Brandenburg.
OSDI 2014.

Race detection for Android applications.

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

Sound Compilation of Reals

Eva Darulova, Viktor Kuncak.
POPL 2014.

Scaling global scheduling with message passing.

Felipe Cerqueira, Manohar Vanga, Björn B. Brandenburg.
RTAS 2014.

A Synchronous IPC Protocol for Predictable Access to Shared Resources in Mixed-Criticality Systems.

Björn B. Brandenburg.
RTSS 2014.

Fast on Average, Predictable in the Worst Case: Exploring Real-Time Futexes in LITMUSRT.

Roy Spliet, Manohar Vanga, Björn B. Brandenburg, Sven Dziadek.
RTSS 2014.

Linux's Processor Affinity API, Refined: Shifting Real-Time Tasks Towards Higher Schedulability.

Felipe Cerqueira, Arpan Gujarati, Björn B. Brandenburg.
RTSS 2014.

On the Complexity of Worst-Case Blocking Analysis of Nested Critical Sections.

Alexander Wieder, Björn B. Brandenburg.
RTSS 2014.

Foundations of Infinite-State Verification.

Rupak Majumdar.
Software Systems Safety 2014.

Asynchronous I-complete approximations.

Anne-Kathrin Schmuck, Jörg Raisch.
Syst. Control. Lett. 2014.

Extending Supervisory Controller Synthesis to Deterministic Pushdown Automata - Enforcing Controllability Least Restrictively.

Anne-Kathrin Schmuck, Sven Schneider, Jörg Raisch, Uwe Nestmann.
WODES 2014.

Reducing an Operational Supervisory Control Problem by Decomposition for Deterministic Pushdown Automata.

Sven Schneider, Anne-Kathrin Schmuck, Uwe Nestmann, Jörg Raisch.
WODES 2014.

On Spin Locks in AUTOSAR: Blocking Analysis of FIFO, Unordered, and Priority-Ordered Spin Locks

Alexander Wieder, Björn B. Brandenburg.
Technical Report MPI-SWS-2013-005 2013.

A Fully Preemptive Multiprocessor Semaphore Protocol for Latency-Sensitive Real-Time Applications

Björn B. Brandenburg.
Technical Report MPI-SWS-2013-003 2013.

Improved Analysis and Evaluation of Real-Time Semaphore Protocols for P-FP Scheduling

Björn B. Brandenburg.
Technical Report MPI-SWS-2013-001 2013.

A theory of robust omega-regular software synthesis.

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

Incremental, Inductive Coverability.

Johannes Kloos, Rupak Majumdar, Filip Niksic, Ruzica Piskac.
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.

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

Rupak Majumdar, Zilong Wang.
CONCUR 2013.

Supervisor synthesis for controller upgrades.

Johannes Kloos, Rupak Majumdar.
DATE 2013.

The OMLP family of optimal multiprocessor real-time locking protocols.

Björn B. Brandenburg, James H. Anderson.
Des. Autom. Embed. Syst. 2013.

A Fully Preemptive Multiprocessor Semaphore Protocol for Latency-Sensitive Real-Time Applications.

Björn B. Brandenburg.
ECRTS 2013.

Outstanding Paper Award: Schedulability Analysis of the Linux Push and Pull Scheduler with Arbitrary Processor Affinities.

Arpan Gujarati, Felipe Cerqueira, Björn B. Brandenburg.
ECRTS 2013.

Cookie	Duration	Description
cookielawinfo-checkbox-analytics	11 months	This cookie is set by GDPR Cookie Consent plugin. The cookie is used to store the user consent for the cookies in the category "Analytics".
cookielawinfo-checkbox-functional	11 months	The cookie is set by GDPR cookie consent to record the user consent for the cookies in the category "Functional".
cookielawinfo-checkbox-necessary	11 months	This cookie is set by GDPR Cookie Consent plugin. The cookies is used to store the user consent for the cookies in the category "Necessary".
cookielawinfo-checkbox-others	11 months	This cookie is set by GDPR Cookie Consent plugin. The cookie is used to store the user consent for the cookies in the category "Other.
cookielawinfo-checkbox-performance	11 months	This cookie is set by GDPR Cookie Consent plugin. The cookie is used to store the user consent for the cookies in the category "Performance".
viewed_cookie_policy	11 months	The cookie is set by the GDPR Cookie Consent plugin and is used to store whether or not user has consented to the use of cookies. It does not store any personal data.