research
∙
09/01/2023
Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete
We investigate the decidability of the 0,∞ fragment of Timed Proposition...
share
research
∙
07/07/2023
Neural Abstraction-Based Controller Synthesis and Deployment
Abstraction-based techniques are an attractive approach for synthesizing...
research
∙
06/29/2023
Generative AI for Programming Education: Benchmarking ChatGPT, GPT-4, and Human Tutors
Generative AI and large language models hold great promise in enhancing ...
research
∙
05/19/2023
Making = Practical: Efficient Interactive Protocols for BDD Algorithms
We show that interactive protocols between a prover and a verifier, a we...
research
∙
01/24/2023
Generating High-Precision Feedback for Programming Syntax Errors using Large Language Models
Large language models (LLMs), such as Codex, hold great promise in enhan...
research
∙
04/26/2022
The Pseudo-Reachability Problem for Diagonalisable Linear Dynamical Systems
We study fundamental reachability problems on pseudo-orbits of linear dy...
research
∙
02/15/2022
Fast Symbolic Algorithms for Omega-Regular Games under Strong Transition Fairness
We consider fixpoint algorithms for two-player games on graphs with ω-re...
research
∙
11/17/2021
Context-Bounded Verification of Thread Pools
Thread pooling is a common programming idiom in which a fixed set of wor...
research
∙
07/08/2021
Generalising Projection in Asynchronous Multiparty Session Types
Multiparty session types (MSTs) provide an efficient methodology for spe...
research
∙
06/09/2021
Bayesian Persuasion in Sequential Decision-Making
We study a dynamic model of Bayesian persuasion in sequential decision-m...
research
∙
05/20/2021
From Verification to Causality-based Explications
In view of the growing complexity of modern software architectures, form...
research
∙
05/19/2021
A Game-Theoretic Account of Responsibility Allocation
When designing or analyzing multi-agent systems, a fundamental problem i...
research
∙
02/25/2021
Subcubic Certificates for CFL Reachability
Many problems in interprocedural program analysis can be modeled as the ...
research
∙
01/21/2021
General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond
The model of asynchronous programming arises in many contexts, from low-...
research
∙
01/04/2021
Lassie: HOL4 Tactics by Example
Proof engineering efforts using interactive theorem proving have yielded...
research
∙
01/04/2021
Symbolic Control for Stochastic Systems via Parity Games
We consider the problem of computing the maximal probability of satisfyi...
research
∙
11/11/2020
The complexity of bounded context switching with dynamic thread creation
Dynamic networks of concurrent pushdown systems (DCPS) are a theoretical...
research
∙
11/09/2020
Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory Programs
We study context-bounded verification of liveness properties of multi-th...
research
∙
11/04/2020
Probabilistic Bisimulation for Parameterized Systems (Technical Report)
Probabilistic bisimulation is a fundamental notion of process equivalenc...
research
∙
10/12/2020
Multiparty Motion Coordination: From Choreographies to Robotics Programs
We present a programming model and typing discipline for complex multi-r...
research
∙
07/03/2020
Supervisory Controller Synthesis for Non-terminating Processes is an Obliging Game
We present a new algorithm to solve the supervisory control problem over...
research
∙
06/09/2020
On Decidability of Time-bounded Reachability in CTMDPs
We consider the time-bounded reachability problem for continuous-time Ma...
research
∙
09/12/2019
Joint Inference of Reward Machines and Policies for Reinforcement Learning
Incorporating high-level knowledge is an effective way to expedite reinf...
research
∙
02/27/2019
Algebraic Invariants for Linear Hybrid Automata
We exhibit an algorithm to compute the strongest algebraic (or polynomia...
research
∙
02/14/2019
Environmentally-friendly GR(1) Synthesis
Many problems in reactive synthesis are stated using two formulas ---an ...
research
∙
02/04/2019
Paracosm: A Language and Tool for Testing Autonomous Driving Systems
Systematic testing of autonomous vehicles operating in complex real-worl...
research
∙
01/21/2019
Perception-in-the-Loop Adversarial Examples
We present a scalable, black box, perception-in-the-loop technique to fi...
research
∙
01/03/2019
Causality Analysis for Concurrent Reactive Systems (Extended Abstract)
We present a comprehensive language theoretic causality analysis framewo...
research
∙
11/20/2018
FAR-Cubicle - A new reachability algorithm for Cubicle
We present a fully automatic algorithm for verifying safety properties o...
research
∙
07/16/2018
Verification of Immediate Observation Population Protocols
Population protocols (Angluin et al., PODC, 2004) are a formal model of ...
research
∙
05/17/2018
Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility
Word equations are a crucial element in the theoretical foundation of co...
research
∙
03/06/2018
Precise but Natural Specification for Robot Tasks
We present Flipper, a natural language interface for describing high lev...
research
∙
10/30/2017
Fair Termination for Parameterized Probabilistic Concurrent Systems (Technical Report)
We consider the problem of automatically verifying that a parameterized ...
research
∙
10/29/2015
Automatic Synthesis of Geometry Problems for an Intelligent Tutoring System
This paper presents an intelligent tutoring system, GeoTutor, for Euclid...
research
∙
11/03/2014
Approximate Counting in SMT and Value Estimation for Probabilistic Programs
#SMT, or model counting for logical theories, is a well-known hard probl...
research
∙
07/04/2012