A5100658822- Logic, programming, and type systems
- Formal Methods in Verification
- Logic, Reasoning, and Knowledge
- semigroups and automata theory
- Machine Learning and Algorithms
- Software Testing and Debugging Techniques
- Semantic Web and Ontologies
- Advanced Algebra and Logic
- Distributed systems and fault tolerance
- Software-Defined Networks and 5G
- Advanced Software Engineering Methodologies
- Advanced Database Systems and Queries
- Computability, Logic, AI Algorithms
- Service-Oriented Architecture and Web Services
- Software Engineering Research
- Bayesian Modeling and Causal Inference
- Optimization and Search Problems
- Natural Language Processing Techniques
- Algorithms and Data Compression
- Petri Nets in System Modeling
- Software System Performance and Reliability
- Polynomial and algebraic computation
- Model-Driven Software Engineering Techniques
- Distributed and Parallel Computing Systems
- Business Process Modeling and Analysis
Cornell University
2021-2025
University College London
2016-2025
Angelina College
2023-2024
University of Oslo
2023
Royal Holloway University of London
2021
École Normale Supérieure de Lyon
2021
Centre National de la Recherche Scientifique
2021
University of Salzburg
2021
University of Pisa
2021
Radboud University Nijmegen
2011-2019
The powerset construction is a standard method for converting nondeterministic automaton into deterministic one recognizing the same language. In this paper, we lift from automata to more general framework of coalgebras with structured state spaces. Coalgebra an abstract uniform study different kinds dynamical systems. An endofunctor F determines both type systems (F-coalgebras) and notion behavioural equivalence (~_F) amongst them. Many types transition their equivalences can be captured by...
Program logics for bug-finding (such as the recently introduced Incorrectness Logic) have framed correctness and incorrectness dual concepts requiring different logical foundations. In this paper, we argue that a single unified theory can be used both reasoning. We present Outcome Logic (OL), novel generalization of Hoare is monadic (to capture computational effects) monoidal reason about outcomes reachability). OL expresses true positive bugs, while retaining reasoning abilities well. To...
Formal Methods (FMs) radically improve the quality of code artefacts they help to produce. They are simple, probably accessible first-year undergraduate students and certainly second-year beyond. Nevertheless, in many cases, not part a general recommendation for course curricula, i.e., taught — yet valuable. One reason this is that teaching “Formal Methods” often confused with logic theory. This article advocates what we call FM thinking : application ideas from applied informal,...
NetKAT is a domain-specific language and logic for specifying verifying network packet-processing functions. It consists of Kleene algebra with tests (KAT) augmented primitives testing modifying packet headers encoding topologies. Previous work developed the design its standard semantics, proved soundness completeness logic, defined PSPACE algorithm deciding equivalence, presented several practical applications.
Separation logic’s compositionality and local reasoning properties have led to significant advances in scalable static analysis. But program analysis has new challenges—many programs display computational effects and, orthogonally, analyzers must handle incorrectness too. We present Outcome Logic (OSL), a logic that is sound for both correctness with varying effects. OSL frame rule—just like separation logic—but uses different underlying assumptions open up larger class of than can be...
In this paper, we present a systematic way of deriving (1) languages (generalised) regular expressions, and (2) sound complete axiomatizations thereof, for wide variety systems. This generalizes both the results Kleene (on deterministic finite automata) Milner behaviours labelled transition systems), includes many other systems such as Mealy Moore machines.
We give a new presentation of Brzozowski's algorithm to minimize finite automata using elementary facts from universal algebra and coalgebra building on earlier work by Arbib Manes categorical Kalman duality between reachability observability. This leads simple proof its correctness opens the door further generalizations. Notably, we derive algorithms obtain minimal language equivalent Moore nondeterministic weighted automata.
Coalgebra is an abstract framework for the uniform study of different kinds dynamical systems. An endofunctor $F$ determines both type systems ($F$-coalgebras) and a notion behavioral equivalence ($\sim_F$) amongst them. Many types transition their equivalences can be captured by functor $F$. For example, deterministic automata derived equivalence language equivalence, while non-deterministic it ordinary bisimilarity. The powerset construction standard method converting nondeterministic...
Coalgebras provide a uniform framework to study dynamical systems, including several types of automata. In this paper, we make use the coalgebraic view on systems investigate, in way, under which conditions calculi that are sound and complete with respect behavioral equivalence can be extended coarser language equivalence, arises from generalised powerset construction determinises coalgebras. We show soundness completeness established by proving expressions modulo axioms calculus form...
We present an Angluin-style algorithm to learn nominal automata, which are acceptors of languages over infinite (structured) alphabets. The abstract approach we take allows us seamlessly extend known variations the this new setting. In particular can a subclass non-deterministic automata. An implementation using recently developed Haskell library for computation is provided preliminary experiments.
Guarded Kleene Algebra with Tests (GKAT) is a variation on (KAT) that arises by restricting the union (+) and iteration (*) operations from KAT to predicate-guarded versions. We develop (co)algebraic theory of GKAT show how it can be efficiently used reason about imperative programs. In contrast KAT, whose equational PSPACE-complete, we (almost) linear time. also provide full theorem prove completeness for an analogue Salomaa’s axiomatization Algebra.
ProbNetKAT is a probabilistic extension of NetKAT with denotational semantics based on Markov kernels. The language expressive enough to generate continuous distributions, which raises the question how compute effectively in language. This paper gives an new characterization ProbNetKAT's using domain theory, provides foundation needed build practical implementation. We show use approximate behavior arbitrary programs distributions finite support. develop prototype implementation and it solve...
Programs increasingly rely on randomization in applications such as cryptography and machine learning. Analyzing randomized programs has been a fruitful research direction, but there is gap when also exploit nondeterminism (for concurrency, efficiency, or algorithmic design). In this paper, we introduce Demonic Outcome Logic for reasoning about that both nondeterminism. The logic includes several novel features, multiple executions tandem manipulating pre- postconditions using familiar...
We present a systematic study of bisimulation-up-to techniques for coalgebras. This enhances the bisimulation proof method large class state based systems, including labelled transition systems but also stream and weighted automata. Our approach allows compositional reasoning about soundness enhancements. Applications include up to bisimilarity, equivalence congruence. All in all, this gives powerful modular framework simplified coinductive proofs equivalence.