2024
Safe POMDP Online Planning Among Dynamic Agents via Adaptive Conformal Prediction.
IEEE Robotics Autom. Lett., November, 2024
Strategy synthesis for zero-sum neuro-symbolic concurrent stochastic games.
Inf. Comput., 2024
BiCert: A Bilinear Mixed Integer Programming Formulation for Precise Certified Bounds Against Data Poisoning Attacks.
CoRR, 2024
Risk-Averse Certification of Bayesian Neural Networks.
CoRR, 2024
PREMAP: A Unifying PREiMage APproximation Framework for Neural Networks.
CoRR, 2024
FullCert: Deterministic End-to-End Certification for Training and Inference of Neural Networks.
CoRR, 2024
Uncertainty-Aware Explanations Through Probabilistic Self-Explainable Neural Networks.
CoRR, 2024
Learning Algorithms for Verification of Markov Decision Processes.
CoRR, 2024
STR-Cert: Robustness Certification for Deep Text Recognition on Deep Learning Pipelines and Vision Transformers.
CoRR, 2024
Probabilistic reach-avoid for Bayesian neural networks.
Artif. Intell., 2024
Provable Preimage Under-Approximation for Neural Networks.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2024
Automated Design of Linear Bounding Functions for Sigmoidal Nonlinearities in Neural Networks.
Proceedings of the Machine Learning and Knowledge Discovery in Databases. Research Track, 2024
HSVI-based online minimax strategies for partially observable stochastic games with neural perception mechanisms.
Proceedings of the 6th Annual Learning for Dynamics & Control Conference, 2024
FAST: Boosting Uncertainty-based Test Prioritization Methods for Neural Networks via Feature Selection.
Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, 2024
The Trembling-Hand Problem for LTLf Planning.
Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, 2024
Trust-Aware Motion Planning for Human-Robot Collaboration under Distribution Temporal Logic Specifications.
Proceedings of the IEEE International Conference on Robotics and Automation, 2024
Learning Decision Policies with Instrumental Variables through Double Machine Learning.
Proceedings of the Forty-first International Conference on Machine Learning, 2024
Partially Observable Stochastic Games with Neural Perception Mechanisms.
Proceedings of the Formal Methods - 26th International Symposium, 2024
Adversarial Robustness Certification for Bayesian Neural Networks.
Proceedings of the Formal Methods - 26th International Symposium, 2024
Strategy Synthesis for Partially Observable Stochastic Games with Neural Perception Mechanisms (Invited Talk).
Proceedings of the 32nd EACSL Annual Conference on Computer Science Logic, 2024
Expectation vs. Reality: Towards Verification of Psychological Games.
Proceedings of the Principles of Verification: Cycling the Probabilistic Landscape, 2024
2023
Physiologically-Informed Gaussian Processes for Interpretable Modelling of Psycho-Physiological States.
IEEE J. Biomed. Health Informatics, August, 2023
Point-based Value Iteration for Neuro-Symbolic POMDPs.
CoRR, 2023
On Preimage Approximation for Neural Networks.
CoRR, 2023
Sample Efficient Model-free Reinforcement Learning from LTL Specifications with Optimality Guarantees.
Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, 2023
When to Trust AI: Advances and Challenges for Certification of Neural Networks.
Proceedings of the 18th Conference on Computer Science and Intelligence Systems, 2023
CONCUR Test-Of-Time Award 2023 (Invited Paper).
Proceedings of the 34th International Conference on Concurrency Theory, 2023
Certifiers Make Neural Networks Vulnerable to Availability Attacks.
Proceedings of the 16th ACM Workshop on Artificial Intelligence and Security, 2023
Compositional Probabilistic and Causal Inference using Tractable Circuit Models.
Proceedings of the International Conference on Artificial Intelligence and Statistics, 2023
2022
PID Control of Biochemical Reaction Networks.
IEEE Trans. Autom. Control., 2022
Adversarial Robustness Guarantees for Gaussian Processes.
J. Mach. Learn. Res., 2022
Bayesian Network Models of Causal Interventions in Healthcare Decision Making: Literature Review and Software Evaluation.
CoRR, 2022
Robustness of Unsupervised Representation Learning without Labels.
CoRR, 2022
Probabilistic Model Checking for Strategic Equilibria-based Decision Making: Advances and Challenges.
CoRR, 2022
Learning Dynamics and Generalization in Reinforcement Learning.
CoRR, 2022
Probabilistic Model Checking and Autonomy.
Annu. Rev. Control. Robotics Auton. Syst., 2022
Finite-horizon equilibria for neuro-symbolic concurrent stochastic games.
Proceedings of the Uncertainty in Artificial Intelligence, 2022
Correlated Equilibria and Fairness in Concurrent Stochastic Games.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022
When are Local Queries Useful for Robust Learning?
Proceedings of the Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, 2022
Probabilistic Model Checking for Strategic Equilibria-Based Decision Making: Advances and Challenges (Invited Talk).
Proceedings of the 47th International Symposium on Mathematical Foundations of Computer Science, 2022
Robustness Guarantees for Credal Bayesian Networks via Constraint Relaxation over Probabilistic Circuits.
Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, 2022
Sample Complexity Bounds for Robustly Learning Decision Lists against Evasion Attacks.
Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, 2022
Individual Fairness Guarantees for Neural Networks.
Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, 2022
Tractable Uncertainty for Structure Learning.
Proceedings of the International Conference on Machine Learning, 2022
Learning Dynamics and Generalization in Deep Reinforcement Learning.
Proceedings of the International Conference on Machine Learning, 2022
Symbolic Verification and Strategy Synthesis for Turn-Based Stochastic Games.
Proceedings of the Principles of Systems Design, 2022
The King Is Naked: On the Notion of Robustness for Natural Language Processing.
Proceedings of the Thirty-Sixth AAAI Conference on Artificial Intelligence, 2022
2021
Formal and Efficient Synthesis for Continuous-Time Linear Stochastic Hybrid Processes.
IEEE Trans. Autom. Control., 2021
Adaptive formal approximations of Markov chains.
Perform. Evaluation, 2021
Automatic verification of concurrent stochastic systems.
Formal Methods Syst. Des., 2021
The EATCS Award 2021 - Laudatio for Toniann (Toni) Pitassi.
Bull. EATCS, 2021
Backdoor Attacks on Network Certification via Data Poisoning.
CoRR, 2021
A Language for Modeling and Optimizing Experimental Biological Protocols.
Comput., 2021
Rational verification: game-theoretic verification of multi-agent systems.
Appl. Intell., 2021
Certification of iterative predictions in Bayesian neural networks.
Proceedings of the Thirty-Seventh Conference on Uncertainty in Artificial Intelligence, 2021
Provable Guarantees on the Robustness of Decision Rules to Causal Interventions.
Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, 2021
On Guaranteed Optimal Robust Explanations for NLP Models.
Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, 2021
Bayesian Inference with Certifiable Adversarial Robustness.
Proceedings of the 24th International Conference on Artificial Intelligence and Statistics, 2021
2020
A game-based approximate verification of deep neural networks with provable guarantees.
Theor. Comput. Sci., 2020
The EATCS Award 2021 - Call for Nominations.
Bull. EATCS, 2020
On the Benefits of Invariance in Neural Networks.
CoRR, 2020
Probabilistic Safety for Bayesian Neural Networks.
Proceedings of the Thirty-Sixth Conference on Uncertainty in Artificial Intelligence, 2020
Multi-player Equilibria Verification for Concurrent Stochastic Games.
Proceedings of the Quantitative Evaluation of Systems - 17th International Conference, 2020
Safety and Robustness for Deep Learning with Provable Guarantees.
Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering, 2020
Uncertainty Quantification with Statistical Guarantees in End-to-End Autonomous Driving Control.
Proceedings of the 2020 IEEE International Conference on Robotics and Automation, 2020
Invariant Causal Prediction for Block MDPs.
Proceedings of the 37th International Conference on Machine Learning, 2020
Assessing Robustness of Text Classification through Maximal Safe Radius Computation.
Proceedings of the Findings of the Association for Computational Linguistics: EMNLP 2020, 2020
Gaussian Processes with Physiologically-Inspired Priors for Physical Arousal Recognition.
Proceedings of the 42nd Annual International Conference of the IEEE Engineering in Medicine & Biology Society, 2020
Robustness Guarantees for Deep Neural Networks on Videos.
Proceedings of the 2020 IEEE/CVF Conference on Computer Vision and Pattern Recognition, 2020
Safety Guarantees for Iterative Predictions with Gaussian Processes.
Proceedings of the 59th IEEE Conference on Decision and Control, 2020
PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time.
Proceedings of the Computer Aided Verification - 32nd International Conference, 2020
Adversarial Robustness Guarantees for Classification with Gaussian Processes.
Proceedings of the 23rd International Conference on Artificial Intelligence and Statistics, 2020
2019
Reasoning about Cognitive Trust in Stochastic Multiagent Systems.
ACM Trans. Comput. Log., 2019
Central Limit Model Checking.
ACM Trans. Comput. Log., 2019
On the Hardness of Robust Classification.
Electron. Colloquium Comput. Complex., 2019
The EATCS Award 2020 - Call for Nominations.
Bull. EATCS, 2019
Safety Guarantees for Planning Based on Iterative Gaussian Processes.
CoRR, 2019
Robustness Quantification for Classification with Gaussian Processes.
CoRR, 2019
Safety and robustness for deep learning with provable guarantees (keynote).
Proceedings of the ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2019
Gaze-based Intention Anticipation over Driving Manoeuvres in Semi-Autonomous Vehicles.
Proceedings of the 2019 IEEE/RSJ International Conference on Intelligent Robots and Systems, 2019
Global Robustness Evaluation of Deep Neural Networks with Provable Guarantees for the Hamming Distance.
Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, 2019
Statistical Guarantees for the Robustness of Bayesian Neural Networks.
Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, 2019
Probabilistic Strategy Logic.
Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, 2019
Efficiency through uncertainty: scalable formal synthesis for stochastic hybrid systems.
Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, 2019
Equilibria-Based Probabilistic Model Checking for Concurrent Stochastic Games.
Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019
Robustness of 3D Deep Learning in an Adversarial Setting.
Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition, 2019
Safety Verification for Deep Neural Networks with Provable Guarantees (Invited Paper).
Proceedings of the 30th International Conference on Concurrency Theory, 2019
Correct-by-Construction Advanced Driver Assistance Systems Based on a Cognitive Architecture.
Proceedings of the IEEE 2nd Connected and Automated Vehicles Symposium, 2019
Verification and Control of Turn-Based Probabilistic Real-Time Games.
Proceedings of the Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy, 2019
Robustness Guarantees for Bayesian Inference with Gaussian Processes.
Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence, 2019
2018
Model Checking Probabilistic Systems.
Proceedings of the Handbook of Model Checking., 2018
Parameter synthesis for probabilistic timed automata using stochastic game abstractions.
Theor. Comput. Sci., 2018
Closed-Loop Quantitative Verification of Rate-Adaptive Pacemakers.
ACM Trans. Cyber Phys. Syst., 2018
PRISM-games: verification and strategy synthesis for stochastic multi-player games with multiple objectives.
Int. J. Softw. Tools Technol. Transf., 2018
Resource-Performance Tradeoff Analysis for Mobile Robots.
IEEE Robotics Autom. Lett., 2018
Chemical reaction network designs for asynchronous logic circuits.
Nat. Comput., 2018
Programming discrete distributions with chemical reaction networks.
Nat. Comput., 2018
Erratum to "Efficient synthesis of robust models for stochastic systems" [The Journal of Systems & Software 143 (2018) 140-158].
J. Syst. Softw., 2018
Efficient synthesis of robust models for stochastic systems.
J. Syst. Softw., 2018
Compositional strategy synthesis for stochastic games with multiple objectives.
Inf. Comput., 2018
Evaluating Uncertainty Quantification in End-to-End Autonomous Driving Control.
CoRR, 2018
Global Robustness Evaluation of Deep Neural Networks with Provable Guarantees for L0 Norm.
CoRR, 2018
Feature-Guided Black-Box Safety Testing of Deep Neural Networks.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018
When Your Fitness Tracker Betrays You: Quantifying the Predictability of Biometric Features Across Contexts.
Proceedings of the 2018 IEEE Symposium on Security and Privacy, 2018
Automated Verification of Concurrent Stochastic Games.
Proceedings of the Quantitative Evaluation of Systems - 15th International Conference, 2018
Calibrating the Classifier: Siamese Neural Network Architecture for End-to-End Arousal Recognition from ECG.
Proceedings of the Machine Learning, Optimization, and Data Science, 2018
Concolic testing for deep neural networks.
Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, 2018
Reachability Analysis of Deep Neural Networks with Provable Guarantees.
Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, 2018
Experimental Biological Protocols with Formal Semantics.
Proceedings of the Computational Methods in Systems Biology, 2018
Automated Recognition of Sleep Arousal Using Multimodal and Personalized Deep Ensembles of Neural Networks.
Proceedings of the Computing in Cardiology, 2018
2017
Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata.
Theor. Comput. Sci., 2017
Precise parameter synthesis for stochastic biochemical systems.
Acta Informatica, 2017
Cognitive Reasoning and Trust in Human-Robot Interactions.
Proceedings of the Theory and Applications of Models of Computation, 2017
RODES: A Robust-Design Synthesis Tool for Probabilistic Systems.
Proceedings of the Quantitative Evaluation of Systems - 14th International Conference, 2017
Broken Hearted: How To Attack ECG Biometrics.
Proceedings of the 24th Annual Network and Distributed System Security Symposium, 2017
Designing Robust Software Systems through Parametric Markov Chain Synthesis.
Proceedings of the 2017 IEEE International Conference on Software Architecture, 2017
Reachability Computation for Switching Diffusions: Finite Abstractions with Certifiable and Tuneable Precision.
Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, 2017
Safety Verification of Deep Neural Networks.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017
Syntax-Guided Optimal Synthesis for Chemical Reaction Networks.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017
Symbolic Verification and Strategy Synthesis for Linearly-Priced Probabilistic Timed Automata.
Proceedings of the Models, Algorithms, Logics and Tools, 2017
A Specification Theory of Real-Time Processes.
Proceedings of the Concurrency, Security, and Puzzles, 2017
Synthesizing Pareto Optimal Decision for Autonomic Clouds Using Stochastic Games Model Checking.
Proceedings of the 24th Asia-Pacific Software Engineering Conference, 2017
Reasoning about Cognitive Trust in Stochastic Multiagent Systems.
Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, 2017
Synthesis and Verification of Self-aware Computing Systems.
,
,
,
,
,
,
,
,
,
,
,
,
Proceedings of the Self-Aware Computing Systems., 2017
2016
Theor. Comput. Sci., 2016
Expected reachability-time games.
Theor. Comput. Sci., 2016
2014 CAV award announcement.
Formal Methods Syst. Des., 2016
Quantitative verification and strategy synthesis for stochastic games.
Eur. J. Control, 2016
The Presburger Award for Young Scientists 2017 - Call for Nominations.
Bull. EATCS, 2016
Resource-Performance Trade-off Analysis for Mobile Robots.
CoRR, 2016
Stochastic analysis of Chemical Reaction Networks using Linear Noise Approximation.
Biosyst., 2016
PRISM-Games 2.0: A Tool for Multi-objective Strategy Synthesis for Stochastic Games.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016
PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016
Approximation of Probabilistic Reachability for Chemical Reaction Networks Using the Linear Noise Approximation.
Proceedings of the Quantitative Evaluation of Systems - 13th International Conference, 2016
Uniform Sampling for Timed Automata with Application to Language Inclusion Measurement.
Proceedings of the Quantitative Evaluation of Systems - 13th International Conference, 2016
Static Program Analysis for Identifying Energy Bugs in Graphics-Intensive Mobile Apps.
Proceedings of the 24th IEEE International Symposium on Modeling, 2016
Model Checking and Strategy Synthesis for Stochastic Games: From Theory to Practice.
Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming, 2016
Building Power Consumption Models from Executable Timed I/O Automata Specifications.
Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, 2016
Advances and challenges of quantitative verification and synthesis for cyber-physical systems.
Proceedings of the 2016 Science of Security for Cyber-Physical Systems Workshop, 2016
A Stochastic Hybrid Approximation for Chemical Kinetics Based on the Linear Noise Approximation.
Proceedings of the Computational Methods in Systems Biology, 2016
Specification revision for Markov decision processes with optimal trade-off.
Proceedings of the 55th IEEE Conference on Decision and Control, 2016
Approximate Policy Iteration for Markov Decision Processes via Quantitative Adaptive Aggregations.
Proceedings of the Automated Technology for Verification and Analysis, 2016
Social Trust: A Major Challenge for the Future of Autonomous Systems.
Proceedings of the 2016 AAAI Fall Symposia, Arlington, Virginia, USA, November 17-19, 2016, 2016
Model Checking Probabilistic Knowledge: A PSPACE Case.
Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, 2016
2015
Computing Cumulative Rewards Using Fast Adaptive Uniformization.
ACM Trans. Model. Comput. Simul., 2015
DNA walker circuits: computational potential, design, and verification.
Nat. Comput., 2015
40th international colloquium on automata, languages and programming.
Inf. Comput., 2015
Simulation-Based Verification of Cardiac Pacemakers With Guaranteed Coverage.
IEEE Des. Test, 2015
Model-driven Algorithms and Architectures for Self-Aware Computing Systems (Dagstuhl Seminar 15041).
Dagstuhl Reports, 2015
Approximate and Probabilistic Computing: Design, Coding, Verification (Dagstuhl Seminar 15491).
Dagstuhl Reports, 2015
Permissive Controller Synthesis for Probabilistic Systems.
Log. Methods Comput. Sci., 2015
Strategy Synthesis for Stochastic Games with Multiple Long-Run Objectives.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015
Parameter synthesis for probabilistic real-time systems (Invited Paper).
Proceedings of the 2nd International Workshop on Synthesis of Complex Parameters, 2015
Synthesising Robust and Optimal Parameters for Cardiac Pacemakers Using Symbolic and Evolutionary Computation Techniques.
Proceedings of the Hybrid Systems Biology - Fourth International Workshop, 2015
Symbolic Minimum Expected Time Controller Synthesis for Probabilistic Timed Automata.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2015
Hardware-in-the-loop simulation and energy optimization of cardiac pacemakers.
Proceedings of the 37th Annual International Conference of the IEEE Engineering in Medicine and Biology Society, 2015
Estimation and Verification of Hybrid Heart Models for Personalised Medical and Wearable Devices.
Proceedings of the Computational Methods in Systems Biology, 2015
Adaptive Aggregation of Markov Chains: Quantitative Analysis of Chemical Reaction Networks.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015
On Quantitative Modelling and Verification of DNA Walker Circuits Using Stochastic Petri Nets.
Proceedings of the Application and Theory of Petri Nets and Concurrency, 2015
2014
Probabilistic Model Checking for Biology.
Proceedings of the Software Systems Safety, 2014
Local abstraction refinement for probabilistic timed programs.
Theor. Comput. Sci., 2014
An algebraic theory of interface automata.
Theor. Comput. Sci., 2014
Compositional assume-guarantee reasoning for input/output component theories.
Sci. Comput. Program., 2014
Quantitative verification of implantable cardiac pacemakers over hybrid heart models.
Inf. Comput., 2014
Automated Verification of Quantitative Properties of Cardiac Pacemaker Software.
Proceedings of the 5th Workshop on Medical Cyber-Physical Systems, 2014
On Quantitative Software Quality Assurance Methodologies for Cardiac Pacemakers.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications, 2014
Formal Modelling and Validation of Rate-Adaptive Pacemakers.
Proceedings of the 2014 IEEE International Conference on Healthcare Informatics, 2014
Synthesising optimal timing delays for Timed I/O Automata.
Proceedings of the 2014 International Conference on Embedded Software, 2014
Compositional Controller Synthesis for Stochastic Games.
Proceedings of the CONCUR 2014 - Concurrency Theory - 25th International Conference, 2014
Precise Parameter Synthesis for Stochastic Biochemical Systems.
Proceedings of the Computational Methods in Systems Biology, 2014
Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014
On Incremental Quantitative Verification for Probabilistic Systems.
Proceedings of the HOWARD-60: A Festschrift on the Occasion of Howard Barringer's 60th Birthday, 2014
Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations.
Proceedings of the Horizons of the Mind. A Tribute to Prakash Panangaden, 2014
Verification of Markov Decision Processes Using Learning Algorithms.
Proceedings of the Automated Technology for Verification and Analysis, 2014
2013
Verification of linear duration properties over continuous-time markov chains.
ACM Trans. Comput. Log., 2013
On the complexity of model checking interval-valued discrete time Markov chains.
Inf. Process. Lett., 2013
From software verification to 'everyware' verification.
Comput. Sci. Res. Dev., 2013
Compositional probabilistic verification through multi-objective model checking.
Inf. Comput., 2013
Automatic verification of competitive stochastic systems.
Formal Methods Syst. Des., 2013
Preface to the special issue on Probabilistic Model Checking.
Formal Methods Syst. Des., 2013
Revisiting Timed Specification Theory II : Realisability
CoRR, 2013
Strategic Analysis of Trust Models for User-Centric Networks
Proceedings of the Proceedings 1st International Workshop on Strategic Reasoning, 2013
Modal Specifications for Probabilistic Timed Systems.
Proceedings of the Proceedings 11th International Workshop on Quantitative Aspects of Programming Languages and Systems, 2013
Model Repair for Markov Decision Processes.
Proceedings of the Seventh International Symposium on Theoretical Aspects of Software Engineering, 2013
PRISM-games: A Model Checker for Stochastic Multi-Player Games.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013
Synthesis for Multi-objective Stochastic Games: An Application to Autonomous Urban Driving.
Proceedings of the Quantitative Evaluation of Systems - 10th International Conference, 2013
A process algebraic framework for estimating the energy consumption in ad-hoc wireless sensor networks.
Proceedings of the 16th ACM International Conference on Modeling, 2013
On Stochastic Games with Multiple Objectives.
Proceedings of the Mathematical Foundations of Computer Science 2013, 2013
Advances in Quantitative Verification for Ubiquitous Computing.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2013, 2013
A simulink hybrid heart model for quantitative verification of cardiac pacemakers.
Proceedings of the 16th international conference on Hybrid systems: computation and control, 2013
Computing Cumulative Rewards Using Fast Adaptive Uniformisation.
Proceedings of the Computational Methods in Systems Biology, 2013
Automated Verification and Strategy Synthesis for Probabilistic Systems.
Proceedings of the Automated Technology for Verification and Analysis, 2013
2012
Advances in Probabilistic Model Checking.
Proceedings of the Software Safety and Security - Tools for Analysis and Verification, 2012
Evaluation of Sustained Stochastic Oscillations by Means of a System of Differential Equations.
Int. J. Comput. Their Appl., 2012
2011 CAV award announcement.
Formal Methods Syst. Des., 2012
Probabilistic verification of Herman's self-stabilisation algorithm.
Formal Aspects Comput., 2012
Optimizing ZigBee Security using Stochastic Model Checking
CoRR, 2012
Large-scale complex IT systems.
Commun. ACM, 2012
Self-adaptive software needs quantitative verification at runtime.
Commun. ACM, 2012
Automatic energy-aware performance analysis of Mobile Ad-Hoc Networks.
Proceedings of the IFIP Wireless Days Conference 2012, Ireland, November 21-23, 2012, 2012
Incremental Runtime Verification of Probabilistic Systems.
Proceedings of the Runtime Verification, Third International Conference, 2012
Quantitative Verification of Implantable Cardiac Pacemakers.
Proceedings of the 33rd IEEE Real-Time Systems Symposium, 2012
The PRISM Benchmark Suite.
Proceedings of the Ninth International Conference on Quantitative Evaluation of Systems, 2012
Towards Communication-Based Steering of Complex Distributed Systems.
Proceedings of the Large-Scale Complex IT Systems. Development, Operation and Management, 2012
Revisiting Timed Specification Theories: A Linear-Time Perspective.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2012
Assume-Guarantee Reasoning for Safe Component Behaviours.
Proceedings of the Formal Aspects of Component Software, 9th International Symposium, 2012
A Compositional Specification Theory for Component Behaviours.
Proceedings of the Programming Languages and Systems, 2012
Playing Stochastic Games Precisely.
Proceedings of the CONCUR 2012 - Concurrency Theory - 23rd International Conference, 2012
Pareto Curves for Probabilistic Model Checking.
Proceedings of the Automated Technology for Verification and Analysis, 2012
2011
OGSA-Based SOA for Collaborative Cancer Research: System Modeling and Generation.
Proceedings of the Guide to e-Science, Next Generation Scientific Research and Discovery, 2011
Dynamic QoS Management and Optimization in Service-Based Systems.
IEEE Trans. Software Eng., 2011
On software verification for sensor nodes.
J. Syst. Softw., 2011
Metamodel-driven SOA for collaborative e-science application.
Comput. Syst. Sci. Eng., 2011
Quantitative Multi-objective Verification for Probabilistic Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2011
Automated Verification Techniques for Probabilistic Systems.
Proceedings of the Formal Methods for Eternal Networked Software Systems, 2011
Partial Order Reduction for Model Checking Markov Decision Processes under Unconditional Fairness.
Proceedings of the Eighth International Conference on Quantitative Evaluation of Systems, 2011
Time-Bounded Verification of CTMCs against Real-Time Specifications.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2011
Automated Learning of Probabilistic Assumptions for Compositional Reasoning.
Proceedings of the Fundamental Approaches to Software Engineering, 2011
Incremental quantitative verification for Markov decision processes.
Proceedings of the 2011 IEEE/IFIP International Conference on Dependable Systems and Networks, 2011
Verifying Team Formation Protocols with Probabilistic Model Checking.
Proceedings of the Computational Logic in Multi-Agent Systems, 2011
PRISM 4.0: Verification of Probabilistic Real-Time Systems.
Proceedings of the Computer Aided Verification - 23rd International Conference, 2011
A Systematic Approach to Evaluate Sustained Stochastic Oscillations.
Proceedings of the ISCA 3rd International Conference on Bioinformatics and Computational Biology, 2011
Learning-Based Compositional Verification for Synchronous Probabilistic Systems.
Proceedings of the Automated Technology for Verification and Analysis, 2011
2010
A biologically inspired QoS routing algorithm for mobile ad hoc networks.
Int. J. Wirel. Mob. Comput., 2010
A game-based abstraction-refinement framework for Markov decision processes.
Formal Methods Syst. Des., 2010
Quantitative Games on Probabilistic Timed Automata
CoRR, 2010
Assume-Guarantee Verification for Probabilistic Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010
Compositional Verification of Probabilistic Systems Using Learning.
Proceedings of the QEST 2010, 2010
Dependability Analysis and Verification for Connected Systems.
Proceedings of the Leveraging Applications of Formal Methods, Verification, and Validation, 2010
Towards a Connector Algebra.
Proceedings of the Leveraging Applications of Formal Methods, Verification, and Validation, 2010
Software verification for TinyOS.
Proceedings of the 9th International Conference on Information Processing in Sensor Networks, 2010
A Framework for Verification of Software with Time and Probabilities.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2010
Parallel Model Checking for Temporal Epistemic Logic.
Proceedings of the ECAI 2010, 2010
10051 Executive Summary - Quantitative and Qualitative Analysis of Network Protocols.
Proceedings of the Quantitative and Qualitative Analysis of Network Protocols, 31.01., 2010
10051 Abstracts Collection - Quantitative and Qualitative Analysis of Network Protocols.
Proceedings of the Quantitative and Qualitative Analysis of Network Protocols, 31.01., 2010
Advances and challenges of probabilistic model checking.
Proceedings of the 48th Annual Allerton Conference on Communication, 2010
2009
Guest Editors' Introduction to the Special Issue on Quantitative Evaluation of Computer Systems.
IEEE Trans. Software Eng., 2009
Probabilistic Mobile Ambients.
Theor. Comput. Sci., 2009
PRISM: probabilistic model checking for performance and reliability analysis.
SIGMETRICS Perform. Evaluation Rev., 2009
Abstraction Refinement for Probabilistic Software.
Proceedings of the Verification, 2009
On Quantitative Software Verification.
Proceedings of the Model Checking Software, 2009
Reo2MC: a tool chain for performance analysis of coordination models.
Proceedings of the 7th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2009
Establishing a Framework for Dynamic Risk Management in 'Intelligent' Aero-Engine Control.
Proceedings of the Computer Safety, 2009
Using quantitative analysis to implement autonomic IT systems.
Proceedings of the 31st International Conference on Software Engineering, 2009
CONNECT Challenges: Towards Emergent Connectors for Eternal Networked Systems.
,
,
,
,
,
,
,
,
,
,
Proceedings of the 14th IEEE International Conference on Engineering of Complex Computer Systems, 2009
Stochastic Games for Verification of Probabilistic Timed Automata.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2009
CADS*: Computer-Aided Development of Self-* Systems.
Proceedings of the Fundamental Approaches to Software Engineering, 2009
Concavely-Priced Probabilistic Timed Automata.
Proceedings of the CONCUR 2009 - Concurrency Theory, 20th International Conference, 2009
Quantitative Verification Techniques for Biological Processes.
Proceedings of the Algorithmic Bioprocesses, 2009
Bug-Free Sensors: The Automatic Verification of Context-Aware TinyOS Applications.
Proceedings of the Ambient Intelligence, 2009
2008
Probabilistic model checking of complex biological pathways.
Theor. Comput. Sci., 2008
Analysis of a gossip protocol in PRISM.
SIGMETRICS Perform. Evaluation Rev., 2008
Using probabilistic model checking in systems biology.
SIGMETRICS Perform. Evaluation Rev., 2008
Multi-Objective Model Checking of Markov Decision Processes.
Log. Methods Comput. Sci., 2008
Game-Based Probabilistic Predicate Abstraction in PRISM.
Proceedings of the Sixth Workshop on Quantitative Aspects of Programming Languages, 2008
Software Engineering Techniques for the Development of Systems of Systems.
Proceedings of the Foundations of Computer Software. Future Trends and Techniques for Development, 2008
Combining Intra- and Inter-cellular Dynamics to Investigate Intestinal Homeostasis.
Proceedings of the Formal Methods in Systems Biology, First International Workshop, 2008
Metamodel-Based Generation of WSRF-Compliant SOA for Collaborative Cancer Research.
Proceedings of the Fourth International Conference on e-Science, 2008
A Biologically Inspired Energy-Aware Routing Algorithm for Communications in Cyberworlds.
Proceedings of the International Conference on Cyberworlds 2008, 2008
WSRF-Based Modeling of Clinical Trial Information for Collaborative Cancer Research.
Proceedings of the 8th IEEE International Symposium on Cluster Computing and the Grid (CCGrid 2008), 2008
2007
Symbolic model checking for probabilistic timed automata.
Inf. Comput., 2007
On Process-algebraic Verification of Asynchronous Circuits.
Fundam. Informaticae, 2007
Quantitative verification: models techniques and tools.
Proceedings of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2007
Stochastic Model Checking.
Proceedings of the Formal Methods for Performance Evaluation, 2007
2006
Numerical vs. statistical probabilistic model checking.
Int. J. Softw. Tools Technol. Transf., 2006
A formal analysis of bluetooth device discovery.
Int. J. Softw. Tools Technol. Transf., 2006
Performance analysis of probabilistic timed automata using digital clocks.
Formal Methods Syst. Des., 2006
Compositional State Space Reduction Using Untangled Actions.
Proceedings of the 13th International Workshop on Expressiveness in Concurrency, 2006
Model checking expected time and expected reward formulae with random time bounds.
Comput. Math. Appl., 2006
Challenges for modeling and simulation methods in systems biology.
Proceedings of the Winter Simulation Conference WSC 2006, 2006
Simulation and verification for computational modelling of signalling pathways.
Proceedings of the Winter Simulation Conference WSC 2006, 2006
PRISM: A Tool for Automatic Verification of Probabilistic Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2006
Game-based Abstraction for Markov Decision Processes.
Proceedings of the Third International Conference on the Quantitative Evaluation of Systems (QEST 2006), 2006
On Reduction Criteria for Probabilistic Reward Models.
Proceedings of the FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 2006
Symmetry Reduction for Probabilistic Model Checking.
Proceedings of the Computer Aided Verification, 18th International Conference, 2006
2005
Evaluating the reliability of NAND multiplexing with PRISM.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2005
Probabilistic model checking in practice: case studies with PRISM.
SIGMETRICS Perform. Evaluation Rev., 2005
Using probabilistic model checking for dynamic power management.
Formal Aspects Comput., 2005
A refinement-based process algebra for timed automata.
Formal Aspects Comput., 2005
A self-organised emergent routing mechanism for mobile ad hoc networks.
Eur. Trans. Telecommun., 2005
Opportunities and Challenges in Process-algebraic Verification of Asynchronous Circuit Designs.
Proceedings of the Second Workshop on Globally Asynchronous, Locally Synchronous Design, 2005
Quantitative Analysis With the Probabilistic Model Checker PRISM.
Proceedings of the Third Workshop on Quantitative Aspects of Programming Languages, 2005
A Biologically Inspired Congestion Control Routing Algorithm for MANETs.
Proceedings of the 3rd IEEE Conference on Pervasive Computing and Communications Workshops (PerCom 2005 Workshops), 2005
Stochastic Transition Systems for Continuous State Spaces and Non-determinism.
Proceedings of the Foundations of Software Science and Computational Structures, 2005
A Timing Analysis of AODV.
Proceedings of the Formal Methods for Open Object-Based Distributed Systems, 2005
A Wavefront Parallelisation of CTMC Solution Using MTBDDs.
Proceedings of the 2005 International Conference on Dependable Systems and Networks (DSN 2005), 28 June, 2005
An MTBDD-Based Implementation of Forward Reachability for Probabilistic Timed Automata.
Proceedings of the Automated Technology for Verification and Analysis, 2005
2004
Probabilistic symbolic model checking with PRISM: a hybrid approach.
Int. J. Softw. Tools Technol. Transf., 2004
Automatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM.
Int. J. Softw. Tools Technol. Transf., 2004
Towards a Unifying CSP approach to Hierarchical Verification of Asynchronous Hardware.
Proceedings of the Fouth International Workshop on Automated Verification of Critical Systems, 2004
Evaluating the Reliability of Defect-Tolerant Architectures for Nanotechnology with Probabilistic Model Checking.
Proceedings of the 17th International Conference on VLSI Design (VLSI Design 2004), 2004
Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004
PRISM 2.0: A Tool for Probabilistic Model Checking.
Proceedings of the 1st International Conference on Quantitative Evaluation of Systems (QEST 2004), 2004
Dual-Processor Parallelisation of Symbolic Probabilistic Model Checking.
Proceedings of the 12th International Workshop on Modeling, 2004
A swarm intelligence routing algorithm for MANETs.
Proceedings of the IASTED International Conference on Communications, Internet, and Information Technology, November 22, 2004
Mathematical techniques for analyzing concurrent and probabilistic systems.
CRM monograph series 23, American Mathematical Society, ISBN: 978-0-8218-3571-5, 2004
2003
On the use of MTBDDs for performability analysis and verification of stochastic systems.
J. Log. Algebraic Methods Program., 2003
Probabilistic Model Checking of Deadline Properties in the IEEE 1394 FireWire Root Contention Protocol.
Formal Aspects Comput., 2003
Model checking for probability and time: from theory to practice .
Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 2003
2002
Automatic verification of real-time systems with discrete probability distributions.
Theor. Comput. Sci., 2002
A Symbolic Out-of-Core Solution Method for Markov Models.
Proceedings of the Parallel and Distributed Model Checking, 2002
Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol.
Proceedings of the Process Algebra and Probabilistic Methods, 2002
Model Checking CSL until Formulae with Random Time Bounds.
Proceedings of the Process Algebra and Probabilistic Methods, 2002
Out-of-Core Solution of Large Linear Systems of Equations Arising from Stochastic Modelling.
Proceedings of the Process Algebra and Probabilistic Methods, 2002
Formal analysis and validation of continuous-time Markov chain based system level power management strategies.
Proceedings of the Seventh IEEE International High-Level Design Validation and Test Workshop 2002, 2002
Verifying Randomized Byzantine Agreement.
Proceedings of the Formal Techniques for Networked and Distributed Systems, 2002
PRISM: Probabilistic Symbolic Model Checker.
Proceedings of the Computer Performance Evaluation, 2002
2001
Faster and Symbolic CTMC Model Checking.
Proceedings of the Process Algebra and Probabilistic Methods, 2001
Symbolic Computation of Maximal Probabilistic Reachability.
Proceedings of the CONCUR 2001, 2001
Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM.
Proceedings of the Computer Aided Verification, 13th International Conference, 2001
2000
On Topological Hierarchies of Temporal Properties.
Fundam. Informaticae, 2000
Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Representation.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 2000
Verifying Quantitative Properties of Continuous Probabilistic Timed Automata.
Proceedings of the CONCUR 2000, 2000
1998
On the Verification of Qualitative Properties of Probabilistic Processes under Fairness Constraints.
Inf. Process. Lett., 1998
A Testing Equivalence for Reactive Probabilistic Processes.
Proceedings of the Fifth International Workshop on Expressiveness in Concurrency, 1998
Computing Probability Bounds for Linear Time Formulas over Concurrent Probabilistic Systems.
Proceedings of the First International Workshop on Probabilistic Methods in Verification, 1998
Proceedings of the First International Workshop on Probabilistic Methods in Verification, 1998
Model Checking for a Probabilistic Branching Time Logic with Fairness.
Distributed Comput., 1998
Comparing CTL and PCTL on labeled Markov chains.
Proceedings of the Programming Concepts and Methods, 1998
1997
A Fully Abstract Metric-Space Denotational Semantics for Reactive Probabilistic Processes
Proceedings of the Third Workshop on Computation and Approximation, 1997
Proceedings of the Third Workshop on Computation and Approximation, 1997
Domain equations for probabilistic processes.
Proceedings of the International Workshop on Expressiveness in Concurrency, 1997
Automatic Verification of Liveness Properties of Randomized Systems.
Proceedings of the Sixteenth Annual ACM Symposium on Principles of Distributed Computing, 1997
Quantitative Analysis and Model Checking.
Proceedings of the Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29, 1997
Symbolic Model Checking for Probabilistic Processes.
Proceedings of the Automata, Languages and Programming, 24th International Colloquium, 1997
1996
Probabilistic Metric Semantics for a Simple Language with Recursion.
Proceedings of the Mathematical Foundations of Computer Science 1996, 1996
1995
Duality and the Completeness of the Modal mu-Calculus.
Theor. Comput. Sci., 1995
Possible and Guaranteed Concurrency in CSP.
Proceedings of the International Workshop on Structures in Concurrency Theory, 1995
1994
Synchronisation Trees and Fairness: A Case Study.
Proceedings of the Proceedings for the Second Imperial College Department of Computing Workshop on Theory and Formal Methods, 1994
A Hierarchy of Partial Order Temporal Properties.
Proceedings of the Temporal Logic, First International Conference, 1994
1993
Concurrency and Conflict in CSP.
Proceedings of the Theory and Formal Methods 1993, 1993
Concurrency, Fairness and Logical Complexity.
Proceedings of the Theory and Formal Methods 1993, 1993
On Duality for the Modal µ-Calculus.
Proceedings of the Computer Science Logic, 7th Workshop, 1993
1992
Infinite Behaviour and Fairness in Concurrent Constraint Programming.
Proceedings of the Sematics: Foundations and Applications, 1992
1991
On the Domain of Traces and Sequential Composition.
Proceedings of the TAPSOFT'91: Proceedings of the International Joint Conference on Theory and Practice of Software Development, 1991
Trade-Offs in True Concurrency: Pomsets and Mazurkiewicz Traces.
Proceedings of the Mathematical Foundations of Programming Semantics, 1991
1990
Inf. Process. Lett., 1990
Defining Process Fairness for Non-Interleaving Concurrency.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1990
1989
Event Fairness and Non-interleaving Concurrency.
Formal Aspects Comput., 1989