Selected Recent Publications

This page contains some representative publications of the group members. For a complete list of each member’s publications please see their individual web page.

C. Başkent, G. McCusker
A History Based Logic for Dynamic Preference Updates Journal of Logic, Language and Information, to appear

C. Başkent and T. M. Ferguson (ed.s),
Graham Priest on Dialetheism and Paraconsistency, Outstanding Contributions to Logic Series (vol. 18), Springer, 2019.

R. Bornat, J. Boender, F. Kammueller, G. Poly and R. Nagarajan
Describing and Simulating Concurrent Quantum Systems, In TACAS ’20: 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Dublin, Ireland, April 2020. LNCS, Springer.

E. Ardeshir-Larijani, S. J. Gay and R. Nagarajan,
Automated Equivalence Checking of Concurrent Quantum Systems, ACM Transactions on Computational Logic, vol. 19, no 4, December 2018.

Ondrej Kuncar and Andrei Popescu
Safety and conservativity of definitions in HOL and Isabelle/HOL.
45th ACM Symposium on Principles of Programming Languages (POPL 2018).

Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu and Dmitriy Traytel.
Foundational nonuniform (co)datatypes for higher-order logic.
32nd ACM/IEEE Symposium on Logic in Computer Science (LICS 2017).

D. Windridge and R. Nagarajan.
Quantum Bootstrap Aggregation.
10th International Quantum Interaction Conference (QI 2016), San Francisco, July 2016. Accepted for publication.

Helmut Alt, Sergio Cabello, Panos Giannopoulos, Cristian Knauer.
Minimum Cell Connection in Line Segment Arrangements.
Int. J. of Computational Geometry and Applications, World Scientific. Accepted for publication.

Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Foundational Extensible Corecursion: A Proof Assistant Perspective
The 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015).

B. Barn, G. Primiero, R. Barn
An Approach to Early Evaluation of Informational Privacy Requirements.
Forthcoming in Proceedings of ACM SAC 2015.

V. De Florio, G. Primiero
A method for trustworthiness assessment based on fidelity in cyber and physical domains. Forthcoming in Proceedings of 2nd International Workshop on Computational Antifragility and Antifragile Engineering (ANTIFRAGILE 2015) co-located with 6th International Conference on Ambient Systems, Networks and Technologies, Procedia Computer Science.

G. Primiero, F. Raimondi
Software Theory Change for resilient near-complete specifications.
Forthcoming in Proceedings of 2nd International Workshop on Computational Antifragility and Antifragile Engineering (ANTIFRAGILE 2015) co-located with 6th International Conference on Ambient Systems, Networks and Technologies, Procedia Computer Science.

L. Floridi, N. Fresco, G. Primiero.
On malfunctioning software, Synthese, DOI: 10.1007/s11229-014-0610-3

N. Alechina, B. Logan, H.N. Nguyen, F. Raimondi.
Symbolic model checking for one-resource RB+-ATL.
To appear in proceedings of IJCAI 2015.

Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel.
Witnessing (Co)datatypes.
ESOP 2015, LNCS 9032, 359-382, Springer.

Andrei Popescu, Grigore Rosu.
Term-Generic Logic.
Theoretical Computer Science 577: 1–24 (2015)

Sergio Cabello and Panos Giannopoulos.
The Complexity of Separating Points in the Plane.
Accepted in Algorithmica, Springer.

J. Boender, M. Georgieva Ivanova, F. Kammüller and G. Primiero.
Modeling Human Behaviour with Higher Order Logic: Insider Threats.
Socio-Technical Aspects of Security and Trust, STAST2014, co-located with CSF’14
in the Vienna Summer of Logic, 2014.

Sudeep Kanav, Peter Lammich, Andrei Popescu.
A Conference Management System with Verified Document Confidentiality.
CAV 2014, LNCS 8559, 167-183, Springer.

F. Kammüller and C. W. Probst.
Invalidating Policies using Structural Information.
Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA),
Special issue on Insider Threats, to appear, 2014.

F. Kammüller and C. W. Probst.
Combining Generated Data Models with Formal Invalidation for Insider Threat Analysis,
IEEE Security and Privacy Workshops, SPW, WRIT’14. 2014.

F. Kammüller.
Verification of DNSsec Delegation Signatures.
21st International IEEE Conference on Telecommunication, IEEE 2014.

J. Boender, F. Kammüller, and R. Nagarajan.
Verification of Quantum Protocols using Coq.
Poster at the 17th Conference on Quantum Information Processing (QIP). 2014.

N. Alechina, B. Logan, H. Nga Nguyen, F. Raimondi,
Decidable Model-Checking for a Resource Logic with Production of Resources
To appear in Proceedings of ECAI 2014, 21st European Conference on Artificial Intelligence.

G.Primiero, F. Raimondi
A typed natural deduction calculus to reason about secure trust
To appear in IEEE Proceedings of PST2014, Twelfth Annual Conference on Privacy, Security and Trust.

K.Androutsopoulos, N. Gorogiannis, M. Loomes, M. Margolis,G. Primiero, F. Raimondi, P. Varsani, N. Weldin, A.Zivanovic
A Racket-Based Robot to Teach First-Year Computer Science
Proceedings of the European Lisp Symposium, 2014.

Ebrahim Ardeshir-Larijani, Simon Gay and Rajagopal Nagarajan
Verification of Concurrent Quantum Protocols by Equivalence Checking, 
In Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS ’14) , Lecture Notes in Computer Science, Volume 8413, pp 500-514, Springer Verlag, 2014.

Timos Antonopoulos, Nikos Gorogiannis, Christoph Haase, Max Kanovich and Joel Ouaknine
Foundations for Decision Problems in Separation Logic with General Inductive Predicates
to appear in FOSSACS 2014.

Jaap Boender and Claudio Sacerdoti Coen
On the correctness of a branch displacement algorithm
To appear in TACAS 2014.

Kelly Androutsopoulos, David Clark, Haitao Dan, Rob Heirons and Mark Harman.
An Analysis of the Relationship between Conditional Entropy and Failed Error Propagation in Software Testing.
In ICSE ’14, May 31 – June 7, 2014, Hyderabad, India.

K. Pouliasis, G.Primiero
J-Calc: A typed lambda calculus for Intuitionistic Justification Logic
Electronic Notes in Theoretical Computer Science, volume 300, pp.71-87, 2014.

Neha Rungta and Franco Raimondi
Modeling and Verification of Multi-agent Systems
Technical briefing at ICSE 2014

Giuseppe Primiero, Franco Raimondi and Neha Rungta
Model Checking Degrees of Belief in a System of Agents
to appear in AAMAS 2014.

Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
Unified Classical Logic Completeness: A Coinductive Pearl.
IJCAR 2014, LNCS 8562, 46-60, Springer.