%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % LOCATIONS: % _missing I do not have it % _gfc it is one of my publications % _book it is a book/journal I own % _inbook in a book/journal I own % _infile in the TOPICS folders % TOPICS % _FMgeneral General articles about formal methods % _FMmodelcheck Model checking % _FMddalgo Decision diagrams and related data structures and algorithms % _FMddredu Techniques to reduce DD size (approximation, iterations, etc.) % _FMswver Software verification % _FMtemplogic Temporal logic % _FMinfinite Infinite state systems % _FMparallel Parallel and distributed algorithms for verification % _FMpetri Verification of Petri net models % _FMpartialord Partial order methods % _FMappl Applications of formal models % _FMtimedstoch Timed and stochastic verification % _FMtools Verification tools % _FMsat SAT solver-based methods % _FMabstract Abstraction-refinement techniques % _petri Petri nets and stochastic Petri nets % _procalgebra Process algebra % _probability Probability theory and practice % _simulation Simulation theory and practice % _dynamic Discrete-event systems, dynamic systems % _markov Markov chain theory % _mclinear Solution of linear systems, esp. MCs % _transient Transient analysis of stochastic models, esp. MCs % _approx Approximations and bounds for stochastic models, esp. MCs % _kronecker Kronecker % _reliability Reliability, Dependability, Performability % _queueing Queueing systems, Queueing networks % _hybrid Hybrid systems % _stochmodels Stochastic modeling applications % _stochtools Stochastic modeling tools % _programming Programming % _swperfeng Software engineering, Software performance % _distributed Parallel and distributed system theory and practice % _algorithms Data structures, algorithms, theory % _web Web, Internet, E-Commerce, QOS % _misc Anything else % KEYWORDS: % SUPPORT Papers in support of proposed research directions %%%%%%%%%%%% JOURNALS @STRING{jacm = "J.\ ACM"} @STRING{cacm = "Comm.\ ACM"} @STRING{acmtcs = "ACM Trans.\ Comp.\ Syst."} @STRING{acmtms = "ACM Trans.\ Math.\ Softw."} @STRING{acmtit = "ACM Trans.\ Internet Tech."} @STRING{acmtomacs = "ACM TOMACS"} @STRING{acmtoplas = "ACM Trans.\ Progr.\ Lang.\ and Syst."} @STRING{acmtdata = "ACM Trans.\ Database Syst."} @STRING{acmcompsurv = "ACM Comp.\ Surv."} @STRING{sigmod = "ACM SIGMOD"} @STRING{acmqueue = "ACM Queue"} @STRING{peva = "Perf.\ Eval."} @STRING{pereview = "ACM SIGMETRICS Perf.\ Eval.\ Rev."} @STRING{fmsd = "Formal Methods in System Design"} @STRING{sttt = "Software Tools for Technology Transfer"} @STRING{ieeecomp = "IEEE Comp."} @STRING{ieeesw = "IEEE Software"} @STRING{ieeetc = "IEEE Trans.\ Comp."} @STRING{ieeetec = "IEEE Trans.\ \ Electr.\ Comp."} @STRING{ieeevt = "IEEE Trans.\ Veh.\ Technol."} @STRING{ieeetse = "IEEE Trans.\ Softw.\ Eng."} @STRING{ieeetr = "IEEE Trans.\ Rel."} @STRING{ieeetpds = "IEEE Trans.\ Par.\ and Distr.\ Syst."} @STRING{ieeetcomm = "IEEE Trans.\ Comm."} @STRING{ieeetsmc = "IEEE Trans.\ Syst., Man, and Cyb."} @STRING{ieeetrau = "IEEE Trans.\ Aut.\ Contr."} @STRING{ieeetcirc = "IEEE Trans.\ Circ.\ and Syst."} @STRING{ieeetcad = "IEEE Trans.\ CAD of Integr.\ Circ. and Syst."} @STRING{ieeetedu = "IEEE Trans.\ Educ."} @STRING{ieeeproc = "Proc.\ of the IEEE"} @STRING{jss = "J.\ Systems\ and Software"} @STRING{jap = "J.\ Appl.\ Prob."} @STRING{jlap = "J.\ Logic \& Algebraic Progr."} @STRING{aap = "Adv.\ Appl.\ Prob."} @STRING{operres = "Oper.\ Res."} @STRING{jpdc = "J.\ Par.\ and Distr.\ Comp."} @STRING{compsurvey = "Computing Surveys"} @STRING{informsjc = "INFORMS J.\ Comp."} @STRING{orsajc = "ORSA J.\ Comp."} @STRING{microrel = "Microelectronics and Reliability"} @STRING{infocomp = "Information and Computation"} @STRING{ipl = "Information Processing Letters"} @STRING{spl = "Statistics \& Probability Letters"} @STRING{cssm = "Comm.\ Stat.\ -- Stochastic Models"} @STRING{stochmod = "Stochastic Models"} @STRING{theocs = "Theoretical Computer Science"} @STRING{actainfo = "Acta Informatica"} @STRING{compnetworks = "Computer Networks"} @STRING{automatica = "Automatica"} @STRING{swpractice = "Software-Practice and Experience"} @STRING{bellsys = "Bell Syst.\ Techn.\ J."} @STRING{ibmjrd = "IBM J.\ Res.\ and Dev."} @STRING{entcs = "Electronic Notes in Theoretical Computer Science"} %%%%%%%%%%%% PUBLISHERS @STRING{acmpress = "ACM Press"} @STRING{ieeepress = "IEEE Press"} @STRING{ieeecspress = "IEEE Comp.\ Soc.\ Press"} @STRING{dekker = "Marcel Dekker, Inc."} @STRING{kluwer = "Kluwer"} @STRING{springer = "Springer-Verlag"} @STRING{cambridge = "Cambridge University Press"} @STRING{chapman = "Chapman \& Hall"} @STRING{wiley = "John Wiley \& Sons"} @STRING{addison = "Addison-Wesley"} %%%%%%%%%%%% INSTITUTIONS @STRING{watson = "IBM T.J.\ Watson Res.\ Center"} @ARTICLE{Bryant1986, AUTHOR = {Bryant, R. E.}, TITLE = {{Graph-based algorithms for boolean function manipulation}}, JOURNAL = ieeetc, VOLUME = 35, NUMBER = 8, PAGES ={677-691}, MONTH = aug, YEAR = 1986, LOCATION = {_infile}, TOPIC = {_FMddalgo}} @ARTICLE{Bryant1992, AUTHOR = {Bryant, R. E.}, TITLE = {{Symbolic boolean manipulation with ordered binary-decision diagrams}}, JOURNAL = acmcompsurv, VOLUME = {24}, NUMBER = {3}, PAGES = {293-318}, YEAR =1992, LOCATION = {_infile}, TOPIC = {_FMddalgo}} @ARTICLE{Burch1992, author = {Burch, J. R. and Clarke, E. M. and McMillan, K. L. and Dilll, D. L. and Hwang, L. J.}, title = "Symbolic model checking: $10^{20}$ states and beyond", JOURNAL = infocomp, year = 1992, VOLUME = 98, pages = {142-170}, LOCATION = {_infile}, TOPIC = {_FMmodelcheck}} @INPROCEEDINGS{Cimatti1999NuSMV, author = "A. Cimatti and E. Clarke and F. Giunchiglia and M. Roveri", title = {{NuSMV: A new symbolic model verifier}}, booktitle = "{CAV}'99", pages = "495--499", editor = "{N. H}albwachs and {D. P}eled", year = "1999", series = "LNCS 1633", address = "{T}rento, {I}taly", publisher = springer, LOCATION = {_missing}, TOPIC = {_FMtools}} @INPROCEEDINGS{GFC-Saturation-2001, AUTHOR = {Ciardo, Gianfranco and Luettgen, Gerald and Siminiceanu, Radu}, TITLE = {{Saturation: An efficient iteration strategy for symbolic state space generation}}, BOOKTITLE = {{Proc.\ Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}}, ADDRESS = {Genova, Italy}, SERIES = {LNCS 2031}, EDITOR = {Margaria, Tiziana and Yi, Wang}, PAGES = {328-342}, PUBLISHER = springer, MONTH = apr, YEAR = 2001, ABSTRACT = { We present a novel algorithm for generating state spaces of asynchronous systems using Multi--valued Decision Diagrams. In contrast to related work, we encode the next--state function of a system not as a single Boolean function, but as cross--products of integer functions. This permits the application of various iteration strategies to build a system's state space. In particular, we introduce a new elegant strategy, called \emph{saturation}, and implement it in the tool SMART. On top of usually performing several orders of magnitude faster than existing BDD--based state--space generators, our algorithm's required peak memory is often close to the final memory needed for storing the overall state space. }, KEYWORDS = {MDD}, LOCATION = {_gfc}} @INPROCEEDINGS{GFC-MDD-improv-2000, AUTHOR = {Ciardo, Gianfranco and Luettgen, Gerald and Siminiceanu, Radu}, TITLE = {{Efficient symbolic state-space construction for asynchronous systems}}, BOOKTITLE = {{Proc.\ 21th Int.\ Conf.\ on Applications and Theory of Petri Nets}}, ADDRESS = {Aarhus, Denmark}, MONTH = jun, SERIES = {LNCS 1825}, EDITOR = {Nielsen, Mogens and Simpson, Dan}, PAGES = {103-122}, PUBLISHER = springer, YEAR = 2000, ABSTRACT = { Many techniques for the verification of reactive systems rely on the analysis of their reachable state spaces. In this paper, a new algorithm for the symbolic generation of the state spaces of asynchronous system models, such as Petri nets, is developed. The algorithm is based on previous work that employs Multi-valued Decision Diagrams for efficiently storing sets of reachable states. In contrast to related approaches, however, it fully exploits event locality, supports intelligent cache management, and achieves faster convergence via advanced iteration control. The algorithm is implemented in the Petri net tool SMART, and run-time results show that it often performs significantly faster than existing state-space generators. }, KEYWORDS = {}, LOCATION = {_gfc}} @ARTICLE{Kam1998, author = {Kam, T. and Villa, T. and Brayton, R.K. and Sangiovanni-Vincentelli, Alberto}, title = {{Multi-valued decision diagrams: theory and applications}}, journal = "Multiple-Valued Logic", year = "1998", VOLUME = "4", number = "1--2", pages = "9--62", LOCATION = {_missing}, TOPIC = {_FMddalgo}}