INFAMY
swMATH ID:  21177 
Software Authors:  Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, Lijun Zhang 
Description:  INFAMY: An InfiniteState Markov Model Checker. The design of complex concurrent systems often involves intricate performance and dependability considerations. Continuoustime Markov chains (CTMCs) are a widely used modeling formalism, where performance and dependability properties are analyzable by model checking. We present INFAMY, a model checker for arbitrarily structured infinitestate CTMCs. It checks probabilistic timing properties expressible in continuous stochastic logic (CSL). Conventional model checkers explore the given model exhaustively, which is often costly, due to state explosion, and impossible if the model is infinite. INFAMY only explores the model up to a finite depth, with the depth bound being computed onthefly. The computation of depth bounds is configurable to adapt to the characteristics of different classes of models. 
Homepage:  http://dl.acm.org/citation.cfm?id=1575113 
Related Software:  PRISM; APMC; SBML Test Suite; SABRE; MARCIE; MRMC; SPIN; BayesDA; StateFlow 
Cited in:  4 Publications 
Standard Articles
1 Publication describing the Software  Year 

INFAMY: an infinitestate Markov model checker Hahn, Ernst Moritz; Hermanns, Holger; Wachter, Björn; Zhang, Lijun 
2009

all
top 5
Cited by 12 Authors
Cited in 2 Serials
1  Formal Methods in System Design 
1  ACM Transactions on Modeling and Computer Simulation 
Cited in 5 Fields
4  Computer science (68XX) 
1  Probability theory and stochastic processes (60XX) 
1  Statistics (62XX) 
1  Numerical analysis (65XX) 
1  Biology and other natural sciences (92XX) 