Browsing University of Waterloo by Author "Vakili, Amirhossein"
Now showing items 1-6 of 6
-
Finite Model Finding Using the Logic of Equality with Uninterpreted Functions
Vakili, Amirhossein; Day, Nancy A. (Springer, 2016)The problem of finite model finding, finding a satisfying model for a set of first-order logic formulas for a finite scope, is an important step in many verification techniques. In MACE-style solvers, the problem is mapped ... -
New Techniques for Static Symmetry Breaking in Many-Sorted Finite Model Finding
Poremba, Joseph; Day, Nancy A.; Vakili, Amirhossein (IEEE, 2023-06-01)Symmetry in finite model finding problems of many-sorted first-order logic (MSFOL) can be exploited to reduce the number of interpretations considered during search, thereby improving solver performance for tools such as ... -
Representing Behavioural Models with Rich Control Structures in SMT-LIB
Day, Nancy A.; Vakili, Amirhossein (University of Waterloo, 2015-09-01)We motivate and present a proposal for how to represent extended finite state machine behavioural models with rich hierarchical states and compositional control structures (e.g., the Statecharts family) in SMT-LIB. Our ... -
Representing hierarchical state machine models in SMT-LIB
Day, Nancy A.; Vakili, Amirhossein (ACM, 2016-05)We motivate and present a proposal for how to represent the syntax of behavioural models written in extended finite-state machine languages with hierarchical states (e.g., the Statecharts family) in SMT-LIB. By including ... -
Temporal Logic Model Checking as Automated Theorem Proving
Vakili, Amirhossein (University of Waterloo, 2016-01-19)Model checking is an automatic technique for the verification of temporal properties of a system. In this technique, a system is represented as a labelled graph and the specification as a temporal logic formula. The core ... -
Transitive-closure-based model checking (TCMC) in Alloy
Farheen, Sabria; Day, Nancy A.; Vakili, Amirhossein; Abbassi, Ali (Springer, 2020-01-03)We present transitive-closure-based model checking (TCMC): a symbolic representation of the semantics of computational tree logic with fairness constraints (CTLFC) for finite models in first-order logic with transitive ...