Search results for "model checking algorithm"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
2	David Walter, Scott Little, Nicholas Seegmiller, Chris J. Myers, Tomohiro Yoneda	Symbolic Model Checking of Analog/Mixed-Signal Circuits.	ASP-DAC	2007	DBLP DOI BibTeX RDF	analog/mixed-signal circuits, Boolean based symbolic model checking algorithm, VHDL-AMS description, labeled hybrid Petri nets, Boolean signals, temporal logic formulas, timed CTL, Boolean variables, Boolean function, binary decision diagram, hardware description language
2	Tingting Han, Taolue Chen, Jian Lu	Structure Analysis for Dynamic Software Architecture Based on Spatial Logic.	COMPSAC	2005	DBLP DOI BibTeX RDF	Model Checking Algorithm, Spatial logic, Dynamic Software Architecture
2	Taolue Chen, Tingting Han, Jian Lu	Towards a Model Logic for p-Calculus.	COMPSAC	2004	DBLP DOI BibTeX RDF	Symbolic Transition Graph, Model Checking Algorithm, Modal Logic, ?-calculus
2	Hiromi Hiraishi	Verification of deadlock free property of high level robot control.	Asian Test Symposium	2000	DBLP DOI BibTeX RDF	deadlock free property, high level robot control, verification algorithm, task control architecture, concurrent robot control processes, symbolic model verifier, symbolic model checking algorithm, robots, formal verification, logic testing, concurrency control, message passing, symbol manipulation, safety properties, liveness properties
2	Bart Vergauwen, Johan Lewi	A Linear Local Model Checking Algorithm for CTL.	CONCUR	1993	DBLP DOI BibTeX RDF
2	Rance Cleaveland, Bernhard Steffen	A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal Mu-Calculus.	CAV	1991	DBLP DOI BibTeX RDF
1	Wihem Arsac, Luca Compagna, Samuel Paul Kaluvuri, Serena Elisa Ponta	Security validation tool for business processes.	SACMAT	2011	DBLP DOI BibTeX RDF
1	Ariel Cohen 0002, Kedar S. Namjoshi, Yaniv Sa'ar, Lenore D. Zuck, Katya I. Kisyova	Parallelizing a Symbolic Compositional Model-Checking Algorithm.	Haifa Verification Conference	2010	DBLP DOI BibTeX RDF
1	Liang Xu, Wei Chen 0018, Yanyan Xu, Wenhui Zhang	Improved Bounded Model Checking for the Universal Fragment of CTL.	J. Comput. Sci. Technol.	2009	DBLP DOI BibTeX RDF	model checking algorithm, ACTL, SAT, software verification, bounded model checking
1	Naoki Kobayashi	Model-checking higher-order functions.	PPDP	2009	DBLP DOI BibTeX RDF	model checking, program verification, higher-order functions, recursion schemes
1	Yakir Vizel, Orna Grumberg	Interpolation-sequence based model checking.	FMCAD	2009	DBLP DOI BibTeX RDF
1	Susanna Donatelli, Serge Haddad, Jeremy Sproston	Model Checking Timed and Stochastic Properties with CSL^{TA}.	IEEE Trans. Software Eng.	2009	DBLP DOI BibTeX RDF
1	Naoki Kobayashi	Types and Recursion Schemes for Higher-Order Program Verification.	APLAS	2009	DBLP DOI BibTeX RDF
1	Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre	LTL Model Checking of Time-Inhomogeneous Markov Chains.	ATVA	2009	DBLP DOI BibTeX RDF
1	Yang Liu 0003, Jun Sun 0001, Jin Song Dong	Scalable Multi-core Model Checking Fairness Enhanced Systems.	ICFEM	2009	DBLP DOI BibTeX RDF
1	Pedro Baltazar, Paulo Mateus	Temporalization of Probabilistic Propositional Logic.	LFCS	2009	DBLP DOI BibTeX RDF
1	Natasha Alechina, Brian Logan, Nguyen Hoang Nga, Abdur Rakib	Expressing Properties of Coalitional Ability under Resource Bounds.	LORI	2009	DBLP DOI BibTeX RDF
1	Carla A. D. M. Delgado, Mario R. F. Benevides	Verification of Epistemic Properties in Probabilistic Multi-Agent Systems.	MATES	2009	DBLP DOI BibTeX RDF
1	David Faragó, Peter H. Schmitt	Improving Non-Progress Cycle Checks.	SPIN	2009	DBLP DOI BibTeX RDF	Non-progress cycles, Model Checking, SPIN, partial order reduction, depth-first search, livelocks
1	Federico Mari, Igor Melatti, Ivano Salvo, Enrico Tronci, Lorenzo Alvisi, Allen Clement, Harry C. Li	Model Checking Coalition Nash Equilibria in MAD Distributed Systems.	SSS	2009	DBLP DOI BibTeX RDF
1	Alexander Schimpf, Stephan Merz, Jan-Georg Smaus	Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL.	TPHOLs	2009	DBLP DOI BibTeX RDF
1	Ou Wei, Arie Gurfinkel, Marsha Chechik	Mixed Transition Systems Revisited.	VMCAI	2009	DBLP DOI BibTeX RDF
1	Kerstin Bauer, Raffaella Gentilini, Klaus Schneider	Property Driven Three-Valued Model Checking on Hybrid Automata.	WoLLIC	2009	DBLP DOI BibTeX RDF
1	Wanwei Liu, Ji Wang, Huowang Chen, Xiaodong Ma, Zhaofei Wang	Symbolic model checking APSL.	Frontiers of Computer Science in China	2009	DBLP DOI BibTeX RDF	tableau approach, extended NuSMV, symbolic model checking, property specification language
1	Jiaqi Zhu, Hanpin Wang, Zhongyuan Xu	A New Temporal Logic CTL[k-QDDC] and Its Verification.	COMPSAC	2008	DBLP DOI BibTeX RDF	branching past, model checking, quantitative
1	Xiangyu Luo, Kaile Su, Abdul Sattar, Yan Chen	Solving Sum and Product Riddle via BDD-Based Model Checking.	Web Intelligence/IAT Workshops	2008	DBLP DOI BibTeX RDF
1	Hua Jiang, Xiang Li	An Improved Algorithm for the Evaluation of Alternating Fixpoint Expressions in the mu-Calculus.	ITNG	2008	DBLP DOI BibTeX RDF	calculation complexity, NP and co-NP problem, Model Checking, mu-Calculus
1	Takashi Kitamura, Huimin Lin	Specifying Properties for Modular Pi-Calculus.	TASE	2008	DBLP DOI BibTeX RDF	Model checking, process algebra, Modal Logics
1	Wanwei Liu, Ji Wang, Huowang Chen, Xiaodong Ma	Symbolic Model Checking APSL.	TASE	2008	DBLP DOI BibTeX RDF	Symbolic model checking, PSL
1	Jefferson O. Andrade, Yukiyoshi Kameyama	A Direct Algorithm for Multi-valued Bounded Model Checking.	ATVA	2008	DBLP DOI BibTeX RDF
1	Farn Wang	Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions.	ATVA	2008	DBLP DOI BibTeX RDF	time progress, model-checking, convex, Timed automaton, concave, TCTL
1	Peter Niebert, Doron Peled, Amir Pnueli	Discriminative Model Checking.	CAV	2008	DBLP DOI BibTeX RDF
1	Sarvani S. Vakkalanka, Ganesh Gopalakrishnan, Robert M. Kirby	Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings.	CAV	2008	DBLP DOI BibTeX RDF
1	Pavlína Vareková, Ivana Cerná	Model Checking of Control-User Component-Based Parametrised Systems.	CBSE	2008	DBLP DOI BibTeX RDF
1	Catalin Dima	Revisiting Satisfiability and Model-Checking for CTLK with Synchrony and Perfect Recall.	CLIMA	2008	DBLP DOI BibTeX RDF
1	Sascha Klüppelholz, Christel Baier	Alternating-Time Stream Logic for Multi-agent Systems.	COORDINATION	2008	DBLP DOI BibTeX RDF
1	Dimitar P. Guelev, Catalin Dima	Model-Checking Strategic Ability and Knowledge of the Past of Communicating Coalitions.	DALT	2008	DBLP DOI BibTeX RDF
1	Joost-Pieter Katoen, Alexandru Mereacre	Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains.	FORMATS	2008	DBLP DOI BibTeX RDF
1	YoungMin Kwon, Gul Agha	LTLC: Linear Temporal Logic for Control.	HSCC	2008	DBLP DOI BibTeX RDF
1	Jean Goubault-Larrecq, Julien Olivain	A Smell of Orchids.	RV	2008	DBLP DOI BibTeX RDF
1	Peter Lamborn, Eric A. Hansen	Layered Duplicate Detection in External-Memory Model Checking.	SPIN	2008	DBLP DOI BibTeX RDF
1	Miguel E. Andrés, Peter van Rossum	Conditional Probabilities over Probabilistic and Nondeterministic Systems.	TACAS	2008	DBLP DOI BibTeX RDF
1	Jiri Barnat, Lubos Brim, Pavel Simecek, M. Weber	Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking.	TACAS	2008	DBLP DOI BibTeX RDF
1	Haibin Zhang, Zhenhua Duan	Symbolic Algorithm Analysis of Rectangular Hybrid Systems.	TAMC	2008	DBLP DOI BibTeX RDF	model checking, temporal logic, hybrid systems, reachability analysis
1	Vijay D'Silva, Mitra Purandare, Daniel Kroening	Approximation Refinement for Interpolation-Based Model Checking.	VMCAI	2008	DBLP DOI BibTeX RDF
1	Hugo Barros, Sérgio Vale Aguiar Campos, Mark A. J. Song, Luis E. Zárate	Exploring Clause Symmetry in a Distributed Bounded Model Checking Algorithm.	ECBS	2007	DBLP DOI BibTeX RDF
1	Taolue Chen, Jian Lu	Probabilistic Alternating-time Temporal Logic and Model Checking Algorithm.	FSKD	2007	DBLP DOI BibTeX RDF
1	Gérard Basler, Daniel Kroening, Georg Weissenbacher	A Complete Bounded Model Checking Algorithm for Pushdown Systems.	Haifa Verification Conference	2007	DBLP DOI BibTeX RDF
1	Conghua Zhou	A compositional symbolic verification framework for concurrent software.	Infoscale	2007	DBLP DOI BibTeX RDF	model checking, composition, abstract, SAT
1	Sylvain Hallé, Roger Villemaire, Omar Cherkaoui, Boubker Ghandour	Model Checking Data-Aware Workflow Properties with CTL-FO+.	EDOC	2007	DBLP DOI BibTeX RDF
1	Gerard J. Holzmann, Dragan Bosnacki	Multi-Core Model Checking with SPIN.	IPDPS	2007	DBLP DOI BibTeX RDF
1	Luca de Alfaro, Krishnendu Chatterjee, Marco Faella, Axel Legay	Qualitative Logics and Equivalences for Probabilistic Systems.	QEST	2007	DBLP DOI BibTeX RDF
1	Susanna Donatelli, Serge Haddad, Jeremy Sproston	CSLTA: an Expressive Logic for Continuous-Time Markov Chains.	QEST	2007	DBLP DOI BibTeX RDF
1	Dang Van Hung, Miaomiao Zhang	On Verification of Probabilistic Timed Automata against Probabilistic Duration Properties.	RTCSA	2007	DBLP DOI BibTeX RDF
1	Mohamed Saleh, Mourad Debbabi	Verifying Security Properties of Cryptoprotocols: A Novel Approach.	SEFM	2007	DBLP DOI BibTeX RDF
1	Conghua Zhou, Shiguang Ju	SAT-based Bounded Model Checking for SE-LTL.	SNPD	2007	DBLP DOI BibTeX RDF
1	Jinzhao Wu, Lin Zhao	Multi-Valued Model Checking via Groebner Basis Approach.	TASE	2007	DBLP DOI BibTeX RDF
1	Chunming Gao, Jin Li, Zhoujun Li, Huowang Chen	Model Checking for BPEL4WS with Time.	APWeb/WAIM Workshops	2007	DBLP DOI BibTeX RDF	Timed Mobile Ambient, model checking, modal logic, BPEL
1	Geng-Dian Huang, Bow-Yaw Wang	Complete SAT-Based Model Checking for Context-Free Processes.	ATVA	2007	DBLP DOI BibTeX RDF
1	David Walter, Scott Little, Chris J. Myers	Bounded Model Checking of Analog and Mixed-Signal Circuits Using an SMT Solver.	ATVA	2007	DBLP DOI BibTeX RDF
1	Nathaniel Charlton, Michael Huth	Hector: Software Model Checking with Cooperating Analysis Plugins.	CAV	2007	DBLP DOI BibTeX RDF
1	François Fages, Aurélien Rizk	On the Analysis of Numerical Data Time Series in Temporal Logic.	CMSB	2007	DBLP DOI BibTeX RDF
1	John Mullins, Raveca Oarga	Model Checking of Extended OCL Constraints on UML Models in SOCLe.	FMOODS	2007	DBLP DOI BibTeX RDF
1	Gabriel Kalyon, Thierry Massart, Cédric Meuter, Laurent Van Begin	Testing Distributed Systems Through Symbolic Model Checking.	FORTE	2007	DBLP DOI BibTeX RDF	global property, model checking of traces, trace checking, testing, asynchronous distributed systems
1	Cong Tian, Zhenhua Duan	Model Checking Propositional Projection Temporal Logic Based on SPIN.	ICFEM	2007	DBLP DOI BibTeX RDF	Propositional Projection Temporal Logic, Model Checking, Verification, Spin, Automaton
1	Roland Axelsson, Martin Lange	Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic.	LPAR	2007	DBLP DOI BibTeX RDF
1	Lubos Brim, Jiri Barnat	Tutorial: Parallel Model Checking.	SPIN	2007	DBLP DOI BibTeX RDF
1	Alberto Lluch-Lafuente	Towards Model Checking Spatial Properties with SPIN.	SPIN	2007	DBLP DOI BibTeX RDF
1	A. Prasad Sistla, Xiaodong Wang, Min Zhou	Checking extended CTL properties using guarded quotient structures.	Formal Methods in System Design	2007	DBLP DOI BibTeX RDF	Symmetric systems, Guarded quotient structures, Model checking, Temporal logic, Program verification, State space reduction
1	Abhay Vardhan, Mahesh Viswanathan	Learning to verify branching time properties.	Formal Methods in System Design	2007	DBLP DOI BibTeX RDF	Verification, Learning, CTL
1	Christopher Robinson-Mallett, Robert M. Hierons, Peter Liggesmeyer	Achieving communication coverage in testing.	ACM SIGSOFT Software Engineering Notes	2006	DBLP DOI BibTeX RDF	timed state-based specifications, distributed systems, conformance testing, coverage criteria
1	Jamal Bentahar, Bernard Moulin, John-Jules Ch. Meyer	A New Model Checking Approach for Verifying Agent Communication Protocols.	CCECE	2006	DBLP DOI BibTeX RDF
1	Davide Cerotti, Susanna Donatelli, András Horváth, Jeremy Sproston	CSL Model Checking for Generalized Stochastic Petri Nets.	QEST	2006	DBLP DOI BibTeX RDF
1	Subramanian K. Iyer, Debashis Sahoo, E. Allen Emerson, Jawahar Jain	On partitioning and symbolic model checking.	IEEE Trans. on CAD of Integrated Circuits and Systems	2006	DBLP DOI BibTeX RDF
1	Zining Cao	Representing and Verifying Temporal Epistemic Properties in Multi-Agent Systems.	CLIMA	2006	DBLP DOI BibTeX RDF
1	Andreas Podelski, Silke Wagner	Model Checking of Hybrid Systems: From Reachability Towards Stability.	HSCC	2006	DBLP DOI BibTeX RDF
1	Taehoon Lee, Gihwon Kwon, Hyuksoo Han	CTL Model Checking for Boolean Program.	ICCSA	2006	DBLP DOI BibTeX RDF
1	Xiangpeng Zhao, Quan Long, Zongyan Qiu	Model Checking Dynamic UML Consistency.	ICFEM	2006	DBLP DOI BibTeX RDF	Simulation, Algorithm, Model Checking, UML, Semantics, Consistency
1	Zining Cao	Model Checking for Real-Time Temporal, Cooperation and Epistemic Properties.	Intelligent Information Processing	2006	DBLP DOI BibTeX RDF	knowledge logic, model checking, cooperation, Real-time temporal logic
1	Zining Cao	Verifying Real-Time Temporal, Cooperation and Epistemic Properties for Uncertain Agents.	MICAI	2006	DBLP DOI BibTeX RDF
1	Alessio Lomuscio, Bozena Wozna, Andrzej Zbrzezny	Bounded Model Checking Real-Time Multi-agent Systems with Clock Differences: Theory and Implementation.	MoChArt	2006	DBLP DOI BibTeX RDF
1	Zining Cao	Model Checking for Epistemic and Temporal Properties of Uncertain Agents.	PRIMA	2006	DBLP DOI BibTeX RDF
1	Stefan Edelkamp, Shahid Jabbar	Large-Scale Directed Model Checking LTL.	SPIN	2006	DBLP DOI BibTeX RDF
1	Harald Fecher, Martin Leucker, Verena Wolf	Don't Know in Probabilistic Systems.	SPIN	2006	DBLP DOI BibTeX RDF
1	Borzoo Bonakdarpour, Sandeep S. Kulkarni, Fuad Abujarad	Brief Announcement: Distributed Synthesis of Fault-Tolerance.	SSS	2006	DBLP DOI BibTeX RDF
1	Peter Niebert, Doron Peled	Efficient Model Checking for LTL with Partial Order Snapshots.	TACAS	2006	DBLP DOI BibTeX RDF
1	Howard Bowman, Rodolfo Gómez	How to stop time stopping.	Formal Asp. Comput.	2006	DBLP DOI BibTeX RDF	Zeno-timelocks, Non-zenoness conditions, Model checking, Timed automata
1	Cornelia P. Inggs, Howard Barringer	CTL* model checking on a shared-memory architecture.	Formal Methods in System Design	2006	DBLP DOI BibTeX RDF	Model checking, Parallel processing, Multiprocessors, Shared memory, Automata
1	Jianhua Zhao, Xuandong Li, Tao Zheng, Guoliang Zheng	Remove Irrelevant Atomic Formulas for Timed Automaton Model Checking.	J. Comput. Sci. Technol.	2006	DBLP DOI BibTeX RDF	model checking, formal method, timed automaton
1	Taolue Chen, Tingting Han, Jian Lu	A Modal Logic for pi-Calculus and Model Checking Algorithm.	Electr. Notes Theor. Comput. Sci.	2005	DBLP DOI BibTeX RDF
1	Mohammad Izadi, Ali Movaghar-Rahimabadi	An Efficient Model Checking Algorithm for a Fragment of µ-Calculus.	SEKE	2005	DBLP BibTeX RDF
1	Christopher Robinson-Mallett, Peter Liggesmeyer, Tilo Mücke, Ursula Goltz	Generating optimal distinguishing sequences with a model checker.	A-MOST	2005	DBLP DOI BibTeX RDF	model checking, verification, test generation, extended finite state machines, distinguishing sequence, state identification
1	Xiushan Feng, Alan J. Hu, Jin Yang	Partitioned model checking from software specifications.	ASP-DAC	2005	DBLP DOI BibTeX RDF
1	Liang Zhang, Mukul R. Prasad, Michael S. Hsiao, Thomas Sidle	Dynamic abstraction using SAT-based BMC.	DAC	2005	DBLP DOI BibTeX RDF	model checking, SAT, abstraction refinement
1	Abhay Vardhan, Mahesh Viswanathan	Learning to verify branching time properties.	ASE	2005	DBLP DOI BibTeX RDF	CTL, computational learning theory, infinite state systems
1	Christopher Robinson-Mallett, Peter Liggesmeyer, Tilo Mücke, Ursula Goltz	Generating optimal distinguishing sequences with a model checker.	ACM SIGSOFT Software Engineering Notes	2005	DBLP DOI BibTeX RDF	model checking, verification, test generation, extended finite state machines, distinguishing sequence, state identification
1	Mihalis Yannakakis, Kousha Etessami	Checking LTL Properties of Recursive Markov Chains.	QEST	2005	DBLP DOI BibTeX RDF
1	Hyeong-Ju Kang, In-Cheol Park	SAT-based unbounded symbolic model checking.	IEEE Trans. on CAD of Integrated Circuits and Systems	2005	DBLP DOI BibTeX RDF
1	Carl-Johan H. Seger, Robert B. Jones, John W. O'Leary, Thomas F. Melham, Mark Aagaard, Clark Barrett, Don Syme	An industrially effective environment for formal hardware verification.	IEEE Trans. on CAD of Integrated Circuits and Systems	2005	DBLP DOI BibTeX RDF
1	Venkatesh Mysore, Carla Piazza, Bud Mishra	Algorithmic Algebraic Model Checking II: Decidability of Semi-algebraic Model Checking and Its Applications to Systems Biology.	ATVA	2005	DBLP DOI BibTeX RDF