Towards First-Order Symbolic Trajectory Evaluation Export

@article{citeulike:6092348, abstract = {Symbolic Trajectory Evaluation (STE) is a symbolic simulation based bounded model checking approach and its computational complexity depends only on the property being checked not on the size of the circuit. In this paper, we study First-order Symbolic Trajectory Evaluation (FSTE). We first present the computation model: Abstract State Machines (ASMs) combined with a partial order over the state space, in which data and data operations are described using abstract sort and uninterpreted function symbols. Second, we devise an FSTE algorithm which is based on implicit state enumeration of an ASM and implemented using Multiway Decision Graphs (MDGs). Finally, an illustrative example is presented to demonstrate the effectiveness of this approach.}, address = {Los Alamitos, CA, USA}, author = {Li, Donglin and Mohamed, Otmane A. and Abed, Sa'ed}, citeulike-article-id = {6092348}, citeulike-linkout-0 = {http://doi.ieeecomputersociety.org/10.1109/ISMVL.2007.57}, citeulike-linkout-1 = {http://dx.doi.org/10.1109/ISMVL.2007.57}, doi = {10.1109/ISMVL.2007.57}, issn = {0195-623X}, journal = {Multiple-Valued Logic, IEEE International Symposium on}, keywords = {stream\_based\_systems}, pages = {53+}, posted-at = {2009-11-10 08:24:08}, priority = {2}, publisher = {IEEE Computer Society}, title = {Towards First-Order Symbolic Trajectory Evaluation}, url = {http://dx.doi.org/10.1109/ISMVL.2007.57}, volume = {0}, year = {2007} }

TY - JOUR ID - citeulike:6092348 L3 - citeulike-article-id:6092348 N2 - Symbolic Trajectory Evaluation (STE) is a symbolic simulation based bounded model checking approach and its computational complexity depends only on the property being checked not on the size of the circuit. In this paper, we study First-order Symbolic Trajectory Evaluation (FSTE). We first present the computation model: Abstract State Machines (ASMs) combined with a partial order over the state space, in which data and data operations are described using abstract sort and uninterpreted function symbols. Second, we devise an FSTE algorithm which is based on implicit state enumeration of an ASM and implemented using Multiway Decision Graphs (MDGs). Finally, an illustrative example is presented to demonstrate the effectiveness of this approach. JF - Multiple-Valued Logic, IEEE International Symposium on SN - 0195-623X AD - Los Alamitos, CA, USA TI - Towards First-Order Symbolic Trajectory Evaluation PB - IEEE Computer Society VL - 0 SP - 53 KW - stream_based_systems AU - Li, Donglin AU - Mohamed, Otmane AU - Abed, Sa'ed PY - 2007/// UR - http://dx.doi.org/10.1109/ISMVL.2007.57 ER -