[{"language":[{"iso":"eng"}],"conference":{"end_date":"1997-06-25","location":"Haifa, Israel","name":"CAV: Computer Aided Verification","start_date":"1997-06-22"},"publication":"9th International Conference on Computer Aided Verification","oa_version":"None","month":"01","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","status":"public","type":"conference","date_published":"1997-01-01T00:00:00Z","publication_identifier":{"isbn":["9783540631668"]},"publist_id":"99","quality_controlled":"1","page":"340 - 351","publisher":"Springer","scopus_import":"1","_id":"4608","author":[{"full_name":"Alur, Rajeev","first_name":"Rajeev","last_name":"Alur"},{"full_name":"Brayton, Robert","last_name":"Brayton","first_name":"Robert"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Qadeer, Shaz","last_name":"Qadeer","first_name":"Shaz"},{"first_name":"Sriram","last_name":"Rajamani","full_name":"Rajamani, Sriram"}],"article_processing_charge":"No","date_created":"2018-12-11T12:09:44Z","publication_status":"published","intvolume":"      1254","alternative_title":["LNCS"],"title":"Partial-order reduction in symbolic state-space exploration","volume":1254,"acknowledgement":"This research was supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA grant NAG2-892, and by the Semiconductor Research Corporation contracts DC-324.036 and DC-324.005.","extern":"1","citation":{"ista":"Alur R, Brayton R, Henzinger TA, Qadeer S, Rajamani S. 1997. Partial-order reduction in symbolic state-space exploration. 9th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 1254, 340–351.","mla":"Alur, Rajeev, et al. “Partial-Order Reduction in Symbolic State-Space Exploration.” <i>9th International Conference on Computer Aided Verification</i>, vol. 1254, Springer, 1997, pp. 340–51, doi:<a href=\"https://doi.org/10.1007/3-540-63166-6_34\">10.1007/3-540-63166-6_34</a>.","short":"R. Alur, R. Brayton, T.A. Henzinger, S. Qadeer, S. Rajamani, in:, 9th International Conference on Computer Aided Verification, Springer, 1997, pp. 340–351.","ieee":"R. Alur, R. Brayton, T. A. Henzinger, S. Qadeer, and S. Rajamani, “Partial-order reduction in symbolic state-space exploration,” in <i>9th International Conference on Computer Aided Verification</i>, Haifa, Israel, 1997, vol. 1254, pp. 340–351.","chicago":"Alur, Rajeev, Robert Brayton, Thomas A Henzinger, Shaz Qadeer, and Sriram Rajamani. “Partial-Order Reduction in Symbolic State-Space Exploration.” In <i>9th International Conference on Computer Aided Verification</i>, 1254:340–51. Springer, 1997. <a href=\"https://doi.org/10.1007/3-540-63166-6_34\">https://doi.org/10.1007/3-540-63166-6_34</a>.","ama":"Alur R, Brayton R, Henzinger TA, Qadeer S, Rajamani S. Partial-order reduction in symbolic state-space exploration. In: <i>9th International Conference on Computer Aided Verification</i>. Vol 1254. Springer; 1997:340-351. doi:<a href=\"https://doi.org/10.1007/3-540-63166-6_34\">10.1007/3-540-63166-6_34</a>","apa":"Alur, R., Brayton, R., Henzinger, T. A., Qadeer, S., &#38; Rajamani, S. (1997). Partial-order reduction in symbolic state-space exploration. In <i>9th International Conference on Computer Aided Verification</i> (Vol. 1254, pp. 340–351). Haifa, Israel: Springer. <a href=\"https://doi.org/10.1007/3-540-63166-6_34\">https://doi.org/10.1007/3-540-63166-6_34</a>"},"year":"1997","date_updated":"2022-08-16T14:09:54Z","day":"01","doi":"10.1007/3-540-63166-6_34","abstract":[{"lang":"eng","text":"State space explosion is a fundamental obstacle in formal verification of designs and protocols. Several techniques for combating this problem have emerged in the past few years, among which two are significant: partial-order reductions and symbolic state space search. In asynchronous systems, interleavings of independent concurrent events are equivalent, and only a representative interleaving needs to be explored to verify local properties. Partial-order methods exploit this redundancy and visit only a subset of the reachable states. Symbolic techniques, on the other hand, capture the transition relation of a system and the set of reachable states as boolean functions. In many cases, these functions can be represented compactly using binary decision diagrams (BDDs). Traditionally, the two techniques have been practiced by two different schools—partial-order methods with enumerative depth-first search for the analysis of asynchronous network protocols, and symbolic breadth-first search for the analysis of synchronous hardware designs. We combine both approaches and develop a method for using partial-order reduction techniques in symbolic BDD-based invariant checking. We present theoretical results to prove the correctness of the method, and experimental results to demonstrate its efficacy."}]},{"citation":{"ama":"Henzinger TA, Ho P, Wong Toi H. HyTech: A model checker for hybrid systems. In: Vol 1254. Springer; 1997:460-463. doi:<a href=\"https://doi.org/10.1007/3-540-63166-6_48\">10.1007/3-540-63166-6_48</a>","apa":"Henzinger, T. A., Ho, P., &#38; Wong Toi, H. (1997). HyTech: A model checker for hybrid systems (Vol. 1254, pp. 460–463). Presented at the CAV: Computer Aided Verification, Haifa, Israel: Springer. <a href=\"https://doi.org/10.1007/3-540-63166-6_48\">https://doi.org/10.1007/3-540-63166-6_48</a>","chicago":"Henzinger, Thomas A, Pei Ho, and Howard Wong Toi. “HyTech: A Model Checker for Hybrid Systems,” 1254:460–63. Springer, 1997. <a href=\"https://doi.org/10.1007/3-540-63166-6_48\">https://doi.org/10.1007/3-540-63166-6_48</a>.","ieee":"T. A. Henzinger, P. Ho, and H. Wong Toi, “HyTech: A model checker for hybrid systems,” presented at the CAV: Computer Aided Verification, Haifa, Israel, 1997, vol. 1254, pp. 460–463.","mla":"Henzinger, Thomas A., et al. <i>HyTech: A Model Checker for Hybrid Systems</i>. Vol. 1254, Springer, 1997, pp. 460–63, doi:<a href=\"https://doi.org/10.1007/3-540-63166-6_48\">10.1007/3-540-63166-6_48</a>.","short":"T.A. Henzinger, P. Ho, H. Wong Toi, in:, Springer, 1997, pp. 460–463.","ista":"Henzinger TA, Ho P, Wong Toi H. 1997. HyTech: A model checker for hybrid systems. CAV: Computer Aided Verification, LNCS, vol. 1254, 460–463."},"year":"1997","date_updated":"2022-08-17T11:06:13Z","day":"01","doi":"10.1007/3-540-63166-6_48","abstract":[{"lang":"eng","text":"A hybrid system consists of a collection of digital programs that interact with each other and with an analog environment. Examples of hybrid systems include medical equipment, manufacturing controllers, automotive controllers, and robots. The formal analysis of the mixed digital-analog nature of these systems requires a model that incorporates the discrete behavior of computer programs with the continuous behavior of environment variables, such as temperature and pressure. Hybrid automata capture both types of behavior by combining finite automata with differential inclusions (i.e. differential inequalities). HyTech is a symbolic model checker for linear hybrid automata, an expressive, yet automatically analyzable, subclass of hybrid automata. A key feature of HyTech is its ability to perform parametric analysis, i.e. to determine the values of design parameters for which a linear hybrid automaton satisfies a temporal requirement."}],"acknowledgement":"This research was supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA grant NAG2-892, and by the SRC contract 95-DC-324.036.","volume":1254,"extern":"1","scopus_import":"1","_id":"4494","author":[{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Ho","first_name":"Pei","full_name":"Ho, Pei"},{"full_name":"Wong Toi, Howard","last_name":"Wong Toi","first_name":"Howard"}],"article_processing_charge":"No","date_created":"2018-12-11T12:09:08Z","publication_status":"published","intvolume":"      1254","title":"HyTech: A model checker for hybrid systems","alternative_title":["LNCS"],"quality_controlled":"1","page":"460 - 463","publisher":"Springer","type":"conference","date_published":"1997-01-01T00:00:00Z","publication_identifier":{"isbn":["9783540631668"]},"publist_id":"235","status":"public","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","oa_version":"None","month":"01","language":[{"iso":"eng"}],"conference":{"location":"Haifa, Israel","end_date":"1997-06-25","name":"CAV: Computer Aided Verification","start_date":"1997-06-22"}}]