Browsing Mathematics (Faculty of) by Author "Vakili, Amirhossein"
Now showing items 1-4 of 4
-
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 ... -
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 ...