Pedro Antonino
Interests
I'm interested in systems verification in general. So far I have worked on techniques to alleviate the state explosion problem arising in the verification of concurrent systems. I'm particularly focused on techniques that are based on the explicit analysis of only small parts (i.e. some components) of a given concurrent system. Most of my work has been carried out using the CSP (Communicating Sequential Processes) process algebra, a very flexible formal notation, and its communicating-labelled-transition-systems operational semantics.
Biography
I did my undergraduate and masters degree in Computer Science under the supervision of Prof. Augusto Sampaio at the Universidade Federal de Pernambuco, Brazil. Currently, I'm in the 3rd year of my PhD in CS at the University of Oxford, being supervised by Prof. Bill Roscoe.
Selected Publications
-
The Automatic Detection of Token Structures and Invariants Using SAT Checking
Pedro Antonino‚ Thomas Gibson−Robinson and A. W. Roscoe
In Axel Legay and Tiziana Margaria, editors, Tools and Algorithms for the Construction and Analysis of Systems: 23rd International Conference‚ TACAS 2017‚ Held as Part of the European Joint Conferences on Theory and Practice of Software‚ ETAPS 2017‚ Uppsala‚ Sweden‚ April 22−29‚ 2017‚ Proceedings‚ Part II. Pages 249–265. Springer Berlin Heidelberg, Berlin‚ Heidelberg. 2017.
Details about The Automatic Detection of Token Structures and Invariants Using SAT Checking | BibTeX data for The Automatic Detection of Token Structures and Invariants Using SAT Checking | DOI (10.1007/978-3-662-54580-5_15) | Link to The Automatic Detection of Token Structures and Invariants Using SAT Checking
-
Tighter reachability criteria for deadlock freedom analysis
Pedro Antonino‚ Thomas Gibson−Robinson and A.W. Roscoe
2016.
Details about Tighter reachability criteria for deadlock freedom analysis | BibTeX data for Tighter reachability criteria for deadlock freedom analysis | Download (pdf) of Tighter reachability criteria for deadlock freedom analysis
-
Efficient deadlock−freedom checking using local analysis and SAT solving
Pedro Antonino‚ Thomas Gibson−Robinson and A.W. Roscoe
In Proceedings of IFM. 2016.
Details about Efficient deadlock−freedom checking using local analysis and SAT solving | BibTeX data for Efficient deadlock−freedom checking using local analysis and SAT solving | Download (pdf) of Efficient deadlock−freedom checking using local analysis and SAT solving