Jeppu, Natasha Yogananda; Melham, Tom; Kroening, Daniel Enhancing active model learning with equivalence checking using simulation relations. (English) Zbl 07815088 Form. Methods Syst. Des. 61, No. 2-3, 164-197 (2022). MSC: 68-XX PDFBibTeX XMLCite \textit{N. Y. Jeppu} et al., Form. Methods Syst. Des. 61, No. 2--3, 164--197 (2022; Zbl 07815088) Full Text: DOI OA License
Pferscher, Andrea; Aichernig, Bernhard K. Fingerprinting and analysis of Bluetooth devices with automata learning. (English) Zbl 07785150 Form. Methods Syst. Des. 61, No. 1, 35-62 (2022). MSC: 68-XX PDFBibTeX XMLCite \textit{A. Pferscher} and \textit{B. K. Aichernig}, Form. Methods Syst. Des. 61, No. 1, 35--62 (2022; Zbl 07785150) Full Text: DOI arXiv OA License
Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Roveri, Marco; Tonetta, Stefano Verification Modulo theories. (English) Zbl 07757158 Form. Methods Syst. Des. 60, No. 3, 452-481 (2022). MSC: 68-XX PDFBibTeX XMLCite \textit{A. Cimatti} et al., Form. Methods Syst. Des. 60, No. 3, 452--481 (2022; Zbl 07757158) Full Text: DOI OA License
Havelund, Klaus; Peled, Doron On monitoring linear temporal properties. (English) Zbl 07757156 Form. Methods Syst. Des. 60, No. 3, 405-425 (2022). MSC: 68-XX PDFBibTeX XMLCite \textit{K. Havelund} and \textit{D. Peled}, Form. Methods Syst. Des. 60, No. 3, 405--425 (2022; Zbl 07757156) Full Text: DOI
André, Étienne; Nguyen, Hoang Gia; Petrucci, Laure; Sun, Jun Distributed parametric model checking timed automata under non-zenoness assumption. (English) Zbl 1522.68294 Form. Methods Syst. Des. 59, No. 1-3, 253-290 (2021). MSC: 68Q60 68Q45 68Q85 PDFBibTeX XMLCite \textit{É. André} et al., Form. Methods Syst. Des. 59, No. 1--3, 253--290 (2021; Zbl 1522.68294) Full Text: DOI
Dureja, Rohit; Rozier, Kristin Y. Incremental design-space model checking via reusable reachable state approximations. (English) Zbl 1492.68085 Form. Methods Syst. Des. 58, No. 3, 375-398 (2021). MSC: 68Q60 68T20 90B20 93C95 PDFBibTeX XMLCite \textit{R. Dureja} and \textit{K. Y. Rozier}, Form. Methods Syst. Des. 58, No. 3, 375--398 (2021; Zbl 1492.68085) Full Text: DOI Link
Beringer, Lennart; Appel, Andrew W. Abstraction and subsumption in modular verification of C programs. (English) Zbl 1505.68023 Form. Methods Syst. Des. 58, No. 1-2, 322-345 (2021). MSC: 68Q60 03B70 68N15 68N30 PDFBibTeX XMLCite \textit{L. Beringer} and \textit{A. W. Appel}, Form. Methods Syst. Des. 58, No. 1--2, 322--345 (2021; Zbl 1505.68023) Full Text: DOI
Kwiatkowska, Marta; Norman, Gethin; Parker, David; Santos, Gabriel Automatic verification of concurrent stochastic systems. (English) Zbl 1505.68025 Form. Methods Syst. Des. 58, No. 1-2, 188-250 (2021). MSC: 68Q60 68Q85 68Q87 91A15 PDFBibTeX XMLCite \textit{M. Kwiatkowska} et al., Form. Methods Syst. Des. 58, No. 1--2, 188--250 (2021; Zbl 1505.68025) Full Text: DOI arXiv
Pani, Thomas; Weissenbacher, Georg; Zuleger, Florian Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free. (English) Zbl 1522.68161 Form. Methods Syst. Des. 57, No. 2, 270-302 (2021). MSC: 68N30 68N19 68Q60 PDFBibTeX XMLCite \textit{T. Pani} et al., Form. Methods Syst. Des. 57, No. 2, 270--302 (2021; Zbl 1522.68161) Full Text: DOI
Fedyukovich, Grigory; Kaufman, Samuel J.; Bodík, Rastislav Learning inductive invariants by sampling from frequency distributions. (English) Zbl 1506.68054 Form. Methods Syst. Des. 56, No. 1-3, 154-177 (2020). MSC: 68Q60 68N30 68Q32 68Q42 PDFBibTeX XMLCite \textit{G. Fedyukovich} et al., Form. Methods Syst. Des. 56, No. 1--3, 154--177 (2020; Zbl 1506.68054) Full Text: DOI
Mathur, Umang; Bauer, Matthew S.; Chadha, Rohit; Sistla, A. Prasad; Viswanathan, Mahesh Exact quantitative probabilistic model checking through rational search. (English) Zbl 1506.68057 Form. Methods Syst. Des. 56, No. 1-3, 90-126 (2020). MSC: 68Q60 60J20 68Q87 90C40 PDFBibTeX XMLCite \textit{U. Mathur} et al., Form. Methods Syst. Des. 56, No. 1--3, 90--126 (2020; Zbl 1506.68057) Full Text: DOI
Gainer, Paul; Linker, Sven; Dixon, Clare; Hustadt, Ullrich; Fisher, Michael Multi-scale verification of distributed synchronisation. (English) Zbl 1506.68009 Form. Methods Syst. Des. 55, No. 3, 171-221 (2020). MSC: 68M14 68Q60 68Q85 PDFBibTeX XMLCite \textit{P. Gainer} et al., Form. Methods Syst. Des. 55, No. 3, 171--221 (2020; Zbl 1506.68009) Full Text: DOI arXiv
Sánchez, César; Schneider, Gerardo; Ahrendt, Wolfgang; Bartocci, Ezio; Bianculli, Domenico; Colombo, Christian; Falcone, Yliès; Francalanza, Adrian; Krstić, Srđan; Lourenço, João M.; Nickovic, Dejan; Pace, Gordon J.; Rufino, Jose; Signoles, Julien; Traytel, Dmitriy; Weiss, Alexander A survey of challenges for runtime verification from advanced application domains (beyond software). (English) Zbl 1425.68268 Form. Methods Syst. Des. 54, No. 3, 279-335 (2019). MSC: 68Q60 PDFBibTeX XMLCite \textit{C. Sánchez} et al., Form. Methods Syst. Des. 54, No. 3, 279--335 (2019; Zbl 1425.68268) Full Text: DOI arXiv
Broy, Manfred Theory and methodology of assumption/commitment based system interface specification and architectural contracts. (English) Zbl 1392.68238 Form. Methods Syst. Des. 52, No. 1, 33-87 (2018). MSC: 68Q60 68M07 68M14 68M20 PDFBibTeX XMLCite \textit{M. Broy}, Form. Methods Syst. Des. 52, No. 1, 33--87 (2018; Zbl 1392.68238) Full Text: DOI
Murawski, Andrzej S.; Tzevelekos, Nikos Algorithmic games for full ground references. (English) Zbl 1392.68147 Form. Methods Syst. Des. 52, No. 3, 277-314 (2018). MSC: 68N30 68N15 68Q45 68Q55 PDFBibTeX XMLCite \textit{A. S. Murawski} and \textit{N. Tzevelekos}, Form. Methods Syst. Des. 52, No. 3, 277--314 (2018; Zbl 1392.68147) Full Text: DOI
Kupferman, Orna; Vardi, Gal On relative and probabilistic finite counterability. (English) Zbl 1390.68433 Form. Methods Syst. Des. 52, No. 2, 117-146 (2018). MSC: 68Q60 03B44 68Q45 PDFBibTeX XMLCite \textit{O. Kupferman} and \textit{G. Vardi}, Form. Methods Syst. Des. 52, No. 2, 117--146 (2018; Zbl 1390.68433) Full Text: DOI Link
Ghassemi, Fatemeh; Fokkink, Wan Model checking mobile ad hoc networks. (English) Zbl 1368.68247 Form. Methods Syst. Des. 49, No. 3, 159-189 (2016). MSC: 68Q60 68M12 68M14 68Q85 PDFBibTeX XMLCite \textit{F. Ghassemi} and \textit{W. Fokkink}, Form. Methods Syst. Des. 49, No. 3, 159--189 (2016; Zbl 1368.68247) Full Text: DOI
Filliâtre, Jean-Christophe; Gondelman, Léon; Paskevich, Andrei The spirit of ghost code. (English) Zbl 1358.68070 Form. Methods Syst. Des. 48, No. 3, 152-174 (2016). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{J.-C. Filliâtre} et al., Form. Methods Syst. Des. 48, No. 3, 152--174 (2016; Zbl 1358.68070) Full Text: DOI HAL
Basin, David; Klaedtke, Felix; Marinovic, Srdjan; Zălinescu, Eugen Monitoring of temporal first-order properties with aggregations. (English) Zbl 1323.68362 Form. Methods Syst. Des. 46, No. 3, 262-285 (2015). MSC: 68Q60 PDFBibTeX XMLCite \textit{D. Basin} et al., Form. Methods Syst. Des. 46, No. 3, 262--285 (2015; Zbl 1323.68362) Full Text: DOI Link
Chatterjee, Krishnendu; Chmelík, Martin; Daca, Przemysław CEGAR for compositional analysis of qualitative properties in Markov decision processes. (English) Zbl 1322.68137 Form. Methods Syst. Des. 47, No. 2, 230-264 (2015). MSC: 68Q87 68Q60 90C40 91A80 PDFBibTeX XMLCite \textit{K. Chatterjee} et al., Form. Methods Syst. Des. 47, No. 2, 230--264 (2015; Zbl 1322.68137) Full Text: DOI
Kroening, Daniel; Lewis, Matt; Weissenbacher, Georg Under-approximating loops in C programs for fast counterexample detection. (English) Zbl 1322.68054 Form. Methods Syst. Des. 47, No. 1, 75-92 (2015). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{D. Kroening} et al., Form. Methods Syst. Des. 47, No. 1, 75--92 (2015; Zbl 1322.68054) Full Text: DOI
Aarts, Fides; Jonsson, Bengt; Uijen, Johan; Vaandrager, Frits Generating models of infinite-state communication protocols using regular inference with abstraction. (English) Zbl 1322.68131 Form. Methods Syst. Des. 46, No. 1, 1-41 (2015). MSC: 68Q60 68M12 68Q45 PDFBibTeX XMLCite \textit{F. Aarts} et al., Form. Methods Syst. Des. 46, No. 1, 1--41 (2015; Zbl 1322.68131) Full Text: DOI
Türker, Uraz Cengiz; Yenigün, Hüsnü Hardness and inapproximability of minimizing adaptive distinguishing sequences. (English) Zbl 1317.68125 Form. Methods Syst. Des. 44, No. 3, 264-294 (2014). MSC: 68Q60 68Q25 68Q45 PDFBibTeX XMLCite \textit{U. C. Türker} and \textit{H. Yenigün}, Form. Methods Syst. Des. 44, No. 3, 264--294 (2014; Zbl 1317.68125) Full Text: DOI
Wei, Kun; Woodcock, Jim; Burns, Alan Modelling temporal behaviour in complex systems with Timebands. (English) Zbl 1291.68271 Form. Methods Syst. Des. 43, No. 3, 520-551 (2013). MSC: 68Q60 68N30 03B70 03B44 PDFBibTeX XMLCite \textit{K. Wei} et al., Form. Methods Syst. Des. 43, No. 3, 520--551 (2013; Zbl 1291.68271) Full Text: DOI Link
Zuliani, Paolo; Platzer, André; Clarke, Edmund M. Bayesian statistical model checking with application to Stateflow/Simulink verification. (English) Zbl 1291.68273 Form. Methods Syst. Des. 43, No. 2, 338-367 (2013). MSC: 68Q60 68Q87 62F10 62F03 PDFBibTeX XMLCite \textit{P. Zuliani} et al., Form. Methods Syst. Des. 43, No. 2, 338--367 (2013; Zbl 1291.68273) Full Text: DOI
Bertrand, N.; Schnoebelen, P. Computable fixpoints in well-structured symbolic model checking. (English) Zbl 1291.68247 Form. Methods Syst. Des. 43, No. 2, 233-267 (2013). MSC: 68Q60 68Q87 PDFBibTeX XMLCite \textit{N. Bertrand} and \textit{P. Schnoebelen}, Form. Methods Syst. Des. 43, No. 2, 233--267 (2013; Zbl 1291.68247) Full Text: DOI
Norman, Gethin; Parker, David; Sproston, Jeremy Model checking for probabilistic timed automata. (English) Zbl 1291.68265 Form. Methods Syst. Des. 43, No. 2, 164-190 (2013). MSC: 68Q60 68Q87 68Q45 PDFBibTeX XMLCite \textit{G. Norman} et al., Form. Methods Syst. Des. 43, No. 2, 164--190 (2013; Zbl 1291.68265) Full Text: DOI Link
Brázdil, Tomáš; Esparza, Javier; Kiefer, Stefan; Kučera, Antonín Analyzing probabilistic pushdown automata. (English) Zbl 1291.68226 Form. Methods Syst. Des. 43, No. 2, 124-163 (2013). MSC: 68Q45 68-02 68Q87 68Q60 PDFBibTeX XMLCite \textit{T. Brázdil} et al., Form. Methods Syst. Des. 43, No. 2, 124--163 (2013; Zbl 1291.68226) Full Text: DOI Link
Baier, Christel (ed.); Kwiatkowska, Marta (ed.) Preface to the special issue on probabilistic model checking. (English) Zbl 1291.68245 Form. Methods Syst. Des. 43, No. 2, 121-123 (2013). MSC: 68Q60 68Q87 00B15 68-06 PDFBibTeX XMLCite \textit{C. Baier} (ed.) and \textit{M. Kwiatkowska} (ed.), Form. Methods Syst. Des. 43, No. 2, 121--123 (2013; Zbl 1291.68245) Full Text: DOI
Chen, Taolue; Forejt, Vojtěch; Kwiatkowska, Marta; Parker, David; Simaitis, Aistis Automatic verification of competitive stochastic systems. (English) Zbl 1291.68252 Form. Methods Syst. Des. 43, No. 1, 61-92 (2013). MSC: 68Q60 68Q87 91A15 03B44 03B48 PDFBibTeX XMLCite \textit{T. Chen} et al., Form. Methods Syst. Des. 43, No. 1, 61--92 (2013; Zbl 1291.68252) Full Text: DOI
André, Étienne; Fribourg, Laurent; Sproston, Jeremy An extension of the inverse method to probabilistic timed automata. (English) Zbl 1291.68240 Form. Methods Syst. Des. 42, No. 2, 119-145 (2013). MSC: 68Q60 68Q87 68Q45 PDFBibTeX XMLCite \textit{É. André} et al., Form. Methods Syst. Des. 42, No. 2, 119--145 (2013; Zbl 1291.68240) Full Text: DOI
Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano SMT-based scenario verification for hybrid systems. (English) Zbl 1284.03216 Form. Methods Syst. Des. 42, No. 1, 46-66 (2013). MSC: 03D05 68Q60 68T20 68Q45 03B44 03D78 PDFBibTeX XMLCite \textit{A. Cimatti} et al., Form. Methods Syst. Des. 42, No. 1, 46--66 (2013; Zbl 1284.03216) Full Text: DOI
Herbreteau, Frédéric; Srivathsan, B.; Walukiewicz, Igor Efficient emptiness check for timed Büchi automata. (English) Zbl 1247.68143 Form. Methods Syst. Des. 40, No. 2, 122-146 (2012). MSC: 68Q45 68Q60 PDFBibTeX XMLCite \textit{F. Herbreteau} et al., Form. Methods Syst. Des. 40, No. 2, 122--146 (2012; Zbl 1247.68143) Full Text: DOI arXiv
Attie, Paul C. On the refinement of liveness properties of distributed systems. (English) Zbl 1233.68160 Form. Methods Syst. Des. 39, No. 1, 1-46 (2011). MSC: 68Q85 68Q45 03B70 PDFBibTeX XMLCite \textit{P. C. Attie}, Form. Methods Syst. Des. 39, No. 1, 1--46 (2011; Zbl 1233.68160) Full Text: DOI arXiv
Delahaye, Benoît; Caillaud, Benoît; Legay, Axel Probabilistic contracts: a compositional reasoning methodology for the design of systems with stochastic and/or non-deterministic aspects. (English) Zbl 1210.93068 Form. Methods Syst. Des. 38, No. 1, 1-32 (2011). MSC: 93E03 68Q87 68Q45 68Q60 90B25 PDFBibTeX XMLCite \textit{B. Delahaye} et al., Form. Methods Syst. Des. 38, No. 1, 1--32 (2011; Zbl 1210.93068) Full Text: DOI
Jeffords, Ralph D.; Heitmeyer, Constance L.; Archer, Myla M.; Leonard, Elizabeth I. Model-based construction and verification of critical systems using composition and partial refinement. (English) Zbl 1209.68321 Form. Methods Syst. Des. 37, No. 2-3, 265-294 (2010). MSC: 68Q60 68T15 PDFBibTeX XMLCite \textit{R. D. Jeffords} et al., Form. Methods Syst. Des. 37, No. 2--3, 265--294 (2010; Zbl 1209.68321) Full Text: DOI
Baier, Christel; Cloth, Lucia; Haverkort, Boudewijn R.; Hermanns, Holger; Katoen, Joost-Pieter Performability assessment by model checking of Markov reward models. (English) Zbl 1209.68309 Form. Methods Syst. Des. 36, No. 1, 1-36 (2010). MSC: 68Q60 PDFBibTeX XMLCite \textit{C. Baier} et al., Form. Methods Syst. Des. 36, No. 1, 1--36 (2010; Zbl 1209.68309) Full Text: DOI
De Wulf, Martin; Doyen, Laurent; Markey, Nicolas; Raskin, Jean-François Robust safety of timed automata. (English) Zbl 1165.68392 Form. Methods Syst. Des. 33, No. 1-3, 45-84 (2008). MSC: 68Q45 PDFBibTeX XMLCite \textit{M. De Wulf} et al., Form. Methods Syst. Des. 33, No. 1--3, 45--84 (2008; Zbl 1165.68392) Full Text: DOI
Ciardo, Gianfranco; Lüttgen, Gerald; Miner, Andrew S. Exploiting interleaving semantics in symbolic state-space generation. (English) Zbl 1118.68533 Form. Methods Syst. Des. 31, No. 1, 63-100 (2007). MSC: 68Q55 PDFBibTeX XMLCite \textit{G. Ciardo} et al., Form. Methods Syst. Des. 31, No. 1, 63--100 (2007; Zbl 1118.68533) Full Text: DOI
Xiong, Haiyan; Curzon, Paul; Tahar, Sofiène; Blandford, Ann Providing a formal linkage between MDG and HOL. (English) Zbl 1112.68096 Form. Methods Syst. Des. 30, No. 2, 83-116 (2007). MSC: 68Q60 68T15 PDFBibTeX XMLCite \textit{H. Xiong} et al., Form. Methods Syst. Des. 30, No. 2, 83--116 (2007; Zbl 1112.68096) Full Text: DOI Link
Chechik, Marsha; Gurfinkel, Arie; Devereux, Benet; Lai, Albert; Easterbrook, Steve Data structures for symbolic multi-valued model-checking. (English) Zbl 1109.68063 Form. Methods Syst. Des. 29, No. 3, 295-344 (2006). MSC: 68Q60 68P05 68T27 03B50 PDFBibTeX XMLCite \textit{M. Chechik} et al., Form. Methods Syst. Des. 29, No. 3, 295--344 (2006; Zbl 1109.68063) Full Text: DOI
Kwiatkowska, Marta; Norman, Gethin; Parker, David; Sproston, Jeremy Performance analysis of probabilistic timed automata using digital clocks. (English) Zbl 1105.68063 Form. Methods Syst. Des. 29, No. 1, 33-78 (2006). MSC: 68Q45 68Q60 PDFBibTeX XMLCite \textit{M. Kwiatkowska} et al., Form. Methods Syst. Des. 29, No. 1, 33--78 (2006; Zbl 1105.68063) Full Text: DOI Link
Fokkink, Wan; Pang, Jun; van de Pol, Jaco Cones and foci: A mechanical framework for protocol verification. (English) Zbl 1103.68652 Form. Methods Syst. Des. 29, No. 1, 1-31 (2006). MSC: 68Q85 PDFBibTeX XMLCite \textit{W. Fokkink} et al., Form. Methods Syst. Des. 29, No. 1, 1--31 (2006; Zbl 1103.68652) Full Text: DOI
Verdejo, Alberto; Martí-Oliet, Narciso Two case studies of semantics execution in Maude: CCS and LOTOS. (English) Zbl 1086.68552 Form. Methods Syst. Des. 27, No. 1-2, 113-172 (2005). MSC: 68Q42 68Q55 68Q60 68Q85 03B70 PDFBibTeX XMLCite \textit{A. Verdejo} and \textit{N. Martí-Oliet}, Form. Methods Syst. Des. 27, No. 1--2, 113--172 (2005; Zbl 1086.68552) Full Text: DOI
Karvi, T.; Tienari, M.; Kaivola, R. Stepwise development of process-algebraic specifications in decorated trace semantics. (English) Zbl 1083.68080 Form. Methods Syst. Des. 26, No. 3, 293-317 (2005). MSC: 68Q85 68Q60 PDFBibTeX XMLCite \textit{T. Karvi} et al., Form. Methods Syst. Des. 26, No. 3, 293--317 (2005; Zbl 1083.68080) Full Text: DOI
Peled, Doron Combining partial-order reductions with on-the-fly model-checking. (English) Zbl 1425.68267 Form. Methods Syst. Des. 8, No. 1, 39-64 (1996). MSC: 68Q60 68Q45 68Q85 PDFBibTeX XMLCite \textit{D. Peled}, Form. Methods Syst. Des. 8, No. 1, 39--64 (1996; Zbl 1425.68267) Full Text: DOI
Inverardi, Paola; Priami, Corrado Automatic verification of distributed systems: the process algebra approach. (English) Zbl 1425.68294 Form. Methods Syst. Des. 8, No. 1, 7-38 (1996). MSC: 68Q85 68Q60 PDFBibTeX XMLCite \textit{P. Inverardi} and \textit{C. Priami}, Form. Methods Syst. Des. 8, No. 1, 7--38 (1996; Zbl 1425.68294) Full Text: DOI
Fantechi, A.; Gnesi, S.; Ristori, G.; Carenini, M.; Vanocchi, M.; Moreschini, P. Assisting requirement formalization by means of natural language translation. (English) Zbl 0800.68648 Form. Methods Syst. Des. 4, No. 3, 243-263 (1994). MSC: 68T50 68T27 PDFBibTeX XMLCite \textit{A. Fantechi} et al., Form. Methods Syst. Des. 4, No. 3, 243--263 (1994; Zbl 0800.68648) Full Text: DOI
Curzon, Paul Deriving correctness properties of compiled code. (English) Zbl 0785.68061 Form. Methods Syst. Des. 3, No. 1-2, 83-115 (1993). MSC: 68Q60 03B70 68N20 PDFBibTeX XMLCite \textit{P. Curzon}, Form. Methods Syst. Des. 3, No. 1--2, 83--115 (1993; Zbl 0785.68061) Full Text: DOI
von Wright, J.; Hekanaho, J.; Luostarinen, P.; Långbacka, T. Mechanizing some advanced refinement concepts. (English) Zbl 0785.68063 Form. Methods Syst. Des. 3, No. 1-2, 49-81 (1993). MSC: 68Q60 68T15 68Q55 PDFBibTeX XMLCite \textit{J. von Wright} et al., Form. Methods Syst. Des. 3, No. 1--2, 49--81 (1993; Zbl 0785.68063) Full Text: DOI