4 papers
Parameterized Verification of Quantum Circuits (Technical Report)
Parosh Aziz Abdulla, Yu-Fang Chen, Michal HeÄko +4
We present the first fully automatic framework for verifying relational properties of parameterized quantum programs, i.e., a program that, given an input size, generates a corresp…
General Decidability Results for Systems with Continuous Counters
A. R. Balasubramanian, Matthew Hague, Rupak Majumdar +2
Counters that hold natural numbers are ubiquitous in modeling and verifying software systems; for example, they model dynamic creation and use of resources in concurrent programs.…
Checking Consistency of Event-driven Traces
Parosh Aziz Abdulla, Mohamed Faouzi Atig, R. Govind +2
Event-driven programming is a popular paradigm where the flow of execution is controlled by two features: (1) shared memory and (2) sending and receiving of messages between multip…
Modulo quantifiers over functional vocabularies extending addition
A. Baskar, A. V. Sreejith, R. S. Thinniyam
We show that first order logic (FO) and first order logic extended with modulo counting quantifiers (FOMOD) over purely functional vocabularies which extend addition, satisfy the C…