×

zbMATH — the first resource for mathematics

Formal Methods in System Design

An International Journal

Short Title: Form. Methods Syst. Des.
Publisher: Springer US, New York, NY
ISSN: 0925-9856; 1572-8102/e
Online: http://link.springer.com/journal/volumesAndIssues/10703
Comments: Indexed cover-to-cover
Documents Indexed: 499 Publications (since 1992)
References Indexed: 390 Publications with 14,235 References.
all top 5

Latest Issues

57, No. 1 (2021)
56, No. 1-3 (2020)
55, No. 3 (2020)
55, No. 2 (2019)
55, No. 1 (2019)
54, No. 3 (2019)
54, No. 2 (2019)
54, No. 1 (2019)
53, No. 3 (2018)
53, No. 2 (2018)
53, No. 1 (2018)
52, No. 3 (2018)
52, No. 2 (2018)
52, No. 1 (2018)
51, No. 3 (2017)
51, No. 2 (2017)
51, No. 1 (2017)
50, No. 2-3 (2017)
50, No. 1 (2017)
49, No. 3 (2016)
49, No. 1-2 (2016)
48, No. 3 (2016)
48, No. 1-2 (2016)
47, No. 3 (2015)
47, No. 2 (2015)
47, No. 1 (2015)
46, No. 3 (2015)
46, No. 2 (2015)
46, No. 1 (2015)
45, No. 3 (2014)
45, No. 2 (2014)
45, No. 1 (2014)
44, No. 3 (2014)
44, No. 2 (2014)
44, No. 1 (2014)
43, No. 3 (2013)
43, No. 2 (2013)
43, No. 1 (2013)
42, No. 3 (2013)
42, No. 2 (2013)
42, No. 1 (2013)
41, No. 3 (2012)
41, No. 2 (2012)
41, No. 1 (2012)
40, No. 3 (2012)
40, No. 2 (2012)
40, No. 1 (2012)
39, No. 3 (2011)
39, No. 2 (2011)
39, No. 1 (2011)
38, No. 3 (2011)
38, No. 2 (2011)
38, No. 1 (2011)
37, No. 2-3 (2010)
37, No. 1 (2010)
36, No. 3 (2010)
36, No. 2 (2010)
36, No. 1 (2010)
35, No. 3 (2009)
35, No. 2 (2009)
35, No. 1 (2009)
34, No. 3 (2009)
34, No. 2 (2009)
34, No. 1 (2009)
33, No. 1-3 (2008)
32, No. 3 (2008)
32, No. 2 (2008)
32, No. 1 (2008)
31, No. 3 (2007)
31, No. 2 (2007)
31, No. 1 (2007)
30, No. 3 (2007)
30, No. 2 (2007)
30, No. 1 (2007)
29, No. 3 (2006)
29, No. 2 (2006)
29, No. 1 (2006)
28, No. 3 (2006)
28, No. 2 (2006)
28, No. 1 (2006)
27, No. 3 (2005)
27, No. 1-2 (2005)
26, No. 3 (2005)
26, No. 2 (2005)
26, No. 1 (2005)
25, No. 2-3 (2004)
25, No. 1 (2004)
24, No. 3 (2004)
24, No. 2 (2004)
24, No. 1 (2004)
23, No. 3 (2003)
23, No. 2 (2003)
23, No. 1 (2003)
22, No. 3 (2003)
22, No. 2 (2003)
22, No. 1 (2003)
21, No. 3 (2002)
21, No. 2 (2002)
21, No. 1 (2002)
20, No. 3 (2002)
...and 20 more Volumes
all top 5

Authors

11 Clarke, Edmund Melson jun.
11 Kröning, Daniel
10 Strichman, Ofer
10 Vardi, Moshe Y.
8 Falcone, Yliès
8 Grumberg, Orna
7 Bouajjani, Ahmed
7 Peled, Doron A.
6 Barrett, Clark W.
6 Henzinger, Thomas A.
6 Kupferman, Orna
6 Larsen, Kim Guldstrand
6 Raskin, Jean-François
6 Sharygina, Natasha
6 Tonetta, Stefano
5 Alur, Rajeev
5 Biere, Armin
5 Chaki, Sagar
5 Chockler, Hana
5 Fribourg, Laurent
5 Gopalakrishnan, Ganesh Lalitha
5 Havelund, Klaus
5 Heyman, Tamir
5 Majumdar, Rupak
5 Reynolds, Andrew
5 Rümmer, Philipp
5 Viswanathan, Mahesh
5 Vojnar, Tomáš
5 Yorav, Karen
4 Abdulla, Parosh Aziz
4 Ben-David, Shoham
4 Bloem, Roderick
4 Chakraborty, Supratik
4 Chatterjee, Krishnendu
4 Cimatti, Alessandro
4 Cook, Byron
4 Dill, David L.
4 Eisner, Cindy
4 Esparza, Javier
4 Grosu, Radu
4 Gurfinkel, Arie
4 Habermehl, Peter
4 Katoen, Joost-Pieter
4 Kwiatkowska, Marta Z.
4 Roşu, Grigore
4 Sangiovanni-Vincentelli, Alberto L.
4 Sankaranarayanan, Sriram
4 Stoller, Scott D.
4 Tinelli, Cesare
4 Tripakis, Stavros
4 Weissenbacher, Georg
3 Abraham, Jacob A.
3 Andersen, Henrik Reif
3 Aziz, Adnan
3 Baier, Christel
3 Bartocci, Ezio
3 Basin, David A.
3 Becker, Bernd
3 Beer, Ilan
3 Benveniste, Albert
3 Bérard, Béatrice
3 Bouyer, Patricia
3 Cabodi, Gianpiero
3 Claesen, Luc
3 Colombo, Christian
3 Damm, Werner
3 Doyen, Laurent
3 Finkbeiner, Bernd
3 Francalanza, Adrian
3 Gastin, Paul
3 Gnesi, Stefania
3 Griggio, Alberto
3 Hermanns, Holger
3 Hunt, Warren A. jun.
3 Iosif, Radu
3 Jéron, Thierry
3 Katz, Shmuel
3 Klaedtke, Felix
3 Kropf, Thomas
3 Kuncak, Viktor
3 Kurshan, Robert P.
3 La Torre, Salvatore
3 Legay, Axel
3 Malik, Sharad
3 Marchand, Hervé
3 McMillan, Kenneth L.
3 Miné, Antoine
3 Mover, Sergio
3 Nickovic, Dejan
3 Norman, Gethin
3 Pace, Gordon J.
3 Păsăreanu, Corina S.
3 Platzer, André
3 Qadeer, Shaz
3 Ranzato, Francesco
3 Reps, Thomas W.
3 Schneider, Klaus
3 Schuster, Assaf
3 Seshia, Sanjit Arunkumar
3 Sifakis, Joseph
...and 944 more Authors

Publications by Year

Citations contained in zbMATH Open

308 Publications have been cited 1,546 times in 1,190 Documents Cited by Year
Bounded model checking using satisfiability solving. Zbl 0985.68038
Clarke, Edmund; Biere, Armin; Raimi, Richard; Zhu, Yunshan
47
2001
Property preserving abstractions for the verification of concurrent systems. Zbl 0829.68053
Loiseaux, C.; Graf, S.; Sifakis, J.; Bouajjani, A.; Bensalem, S.
38
1995
LSCs: Breathing life into message sequence charts. Zbl 0985.68033
Damm, Werner; Harel, David
34
2001
A linear-time model-checking algorithm for the alternation-free modal mu- calculus. Zbl 0772.68038
Cleaveland, Rance; Steffen, Bernhard
33
1993
An improvement of McMillan’s unfolding algorithm. Zbl 1017.68085
Esparza, Javier; Römer, Stefan; Vogler, Walter
32
2002
Model checking of safety properties. Zbl 0995.68061
Kupferman, Orna; Vardi, Moshe Y.
32
2001
Using partial orders for the efficient verification of deadlock freedom and safety properties. Zbl 0772.68064
Godefroid, Patrice; Wolper, Pierre
30
1993
Faster algorithms for mean-payoff games. Zbl 1213.68430
Brim, L.; Chaloupka, J.; Doyen, L.; Gentilini, R.; Raskin, J. F.
28
2011
Unified QBF certification and its applications. Zbl 1284.68516
Balabanov, Valeriy; Jiang, Jie-Hong R.
25
2012
Performance analysis of probabilistic timed automata using digital clocks. Zbl 1105.68063
Kwiatkowska, Marta; Norman, Gethin; Parker, David; Sproston, Jeremy
23
2006
Using forward reachability analysis for verification of lossy channel systems. Zbl 1073.68675
Abdulla, Parosh Aziz; Collomb-Annichini, Aurore; Bouajjani, Ahmed; Jonsson, Bengt
22
2004
Forward analysis of updatable timed automata. Zbl 1073.68041
Bouyer, Patricia
21
2004
A technique of state space search based on unfolding. Zbl 0829.68085
McMillan, K. L.
21
1995
Analysis of timed systems using time-abstracting bisimulations. Zbl 0971.68096
Tripakis, Stavros; Yovine, Sergio
20
2001
Minimum and maximum delay problems in real-time systems. Zbl 0777.68045
Courcoubetis, Costas; Yannakakis, Mihalis
20
1992
A stubborn attack on state explosion. Zbl 0783.68083
Valmari, Antti
19
1992
An algorithm for strongly connected component analysis in \(n \log n\) symbolic steps. Zbl 1110.68161
Bloem, Roderick; Gabow, Harold N.; Somenzi, Fabio
19
2006
From liveness to promptness. Zbl 1192.68416
Kupferman, Orna; Piterman, Nir; Vardi, Moshe Y.
17
2009
Efficiently solving quantified bit-vector formulas. Zbl 1284.03212
Wintersteiger, Christoph M.; Hamadi, Youssef; De Moura, Leonardo
16
2013
Checking timed Büchi automata emptiness efficiently. Zbl 1085.68083
Tripakis, Stavros; Yovine, Sergio; Bouajjani, Ahmed
16
2005
Synthesis of opaque systems with static and dynamic masks. Zbl 1247.68161
Cassez, Franck; Dubreil, Jérémy; Marchand, Hervé
15
2012
Decision problems for lower/upper bound parametric timed automata. Zbl 1186.68245
Bozzelli, Laura; La Torre, Salvatore
15
2009
Efficient detection of vacuity in temporal model checking. Zbl 0988.68111
Beer, Ilan; Ben-David, Shoham; Eisner, Cindy; Rodeh, Yoav
14
2001
Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness. Zbl 1185.68405
Bagnara, Roberto; Hill, Patricia M.; Zaffanella, Enea
14
2009
Constructing invariants for hybrid systems. Zbl 1133.68365
Sankaranarayanan, Sriram; Sipma, Henny B.; Manna, Zohar
14
2008
A game-based abstraction-refinement framework for Markov decision processes. Zbl 1233.90276
Kattenbelt, Mark; Kwiatkowska, Marta; Norman, Gethin; Parker, David
14
2010
Constraint-based verification of parameterized cache coherence protocols. Zbl 1073.68518
Delzanno, Giorgio
13
2003
Predicate abstraction of ANSI-C programs using SAT. Zbl 1090.68022
Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen
13
2004
Antichains and compositional algorithms for LTL synthesis. Zbl 1258.03046
Filiot, Emmanuel; Jin, Naiyong; Raskin, Jean-François
13
2011
Data structures for symbolic multi-valued model-checking. Zbl 1109.68063
Chechik, Marsha; Gurfinkel, Arie; Devereux, Benet; Lai, Albert; Easterbrook, Steve
13
2006
HySAT: An efficient proof engine for bounded model checking of hybrid systems. Zbl 1116.68048
Fränzle, Martin; Herde, Christian
13
2007
Robust safety of timed automata. Zbl 1165.68392
De Wulf, Martin; Doyen, Laurent; Markey, Nicolas; Raskin, Jean-François
13
2008
On the optimal reachability problem of weighted timed automata. Zbl 1129.68039
Bouyer, Patricia; Brihaye, Thomas; Bruyère, Véronique; Raskin, Jean-François
13
2007
Abstractions for hybrid systems. Zbl 1133.68368
Tiwari, Ashish
13
2008
Why does Astrée scale up? Zbl 1185.68241
Cousot, Patrick; Cousot, Radhia; Feret, Jérôme; Mauborgne, Laurent; Miné, Antoine; Rival, Xavier
12
2009
Partial-order reduction in symbolic state-space exploration. Zbl 1001.68080
Alur, R.; Brayton, R. K.; Henzinger, T. A.; Qadeer, S.; Rajamani, S. K.
11
2001
Optimal infinite scheduling for multi-priced timed automata. Zbl 1133.68360
Bouyer, Patricia; Brinksma, Ed; Larsen, Kim G.
11
2008
A compositional modelling and analysis framework for stochastic hybrid systems. Zbl 1291.68293
Hahn, Ernst Moritz; Hartmanns, Arnd; Hermanns, Holger; Katoen, Joost-Pieter
11
2013
Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning. Zbl 1147.68053
Păsăreanu, Corina S.; Giannakopoulou, Dimitra; Bobaru, Mihaela Gheorghiu; Cobleigh, Jamieson M.; Barringer, Howard
10
2008
Computable fixpoints in well-structured symbolic model checking. Zbl 1291.68247
Bertrand, N.; Schnoebelen, P.
10
2013
Causal semantics for the algebra of connectors. Zbl 1207.68203
Bliudze, Simon; Sifakis, Joseph
10
2010
Automating the addition of fault tolerance with discrete controller synthesis. Zbl 1186.68051
Girault, Alain; Rutten, Éric
9
2009
Combining partial-order reductions with on-the-fly model-checking. Zbl 1425.68267
Peled, Doron
9
1996
Practical interruptible conversations: distributed dynamic verification with multiparty session types and Python. Zbl 1341.68118
Demangeon, Romain; Honda, Kohei; Hu, Raymond; Neykova, Rumyana; Yoshida, Nobuko
9
2015
Two case studies of semantics execution in Maude: CCS and LOTOS. Zbl 1086.68552
Verdejo, Alberto; Martí-Oliet, Narciso
9
2005
Checking finite traces using alternating automata. Zbl 1073.68053
Finkbeiner, Bernd; Sipma, Henny
8
2004
Java-MaC: A run-time assurance approach for Java programs. Zbl 1073.68552
Kim, MoonZoo; Viswanathan, Mahesh; Kannan, Sampath; Lee, Insup; Sokolsky, Oleg
8
2004
An overview of the runtime verification tool Java PathExplorer. Zbl 1073.68549
Havelund, Klaus; Roşu, Grigore
8
2004
Reducing concurrent analysis under a context bound to sequential analysis. Zbl 1186.68298
Lal, Akash; Reps, Thomas
8
2009
Specification and analysis of the AER/NCA active network protocol suite in real-time Maude. Zbl 1109.68010
Ölveczky, Peter Csaba; Meseguer, José; Talcott, Carolyn L.
8
2006
Synthesising correct concurrent runtime monitors. Zbl 1323.68373
Francalanza, Adrian; Seychell, Aldrin
8
2015
SMT-based model checking for recursive programs. Zbl 1358.68072
Komuravelli, Anvesh; Gurfinkel, Arie; Chaki, Sagar
8
2016
Bisimulation minimization and symbolic model checking. Zbl 1018.68052
Fisler, Kathi; Vardi, Moshe Y.
7
2002
Parallelizing the \(\text{Mur}\varphi\) verifier. Zbl 1001.68073
Stern, Ulrich; Dill, David
7
2001
Dynamic partitioning in linear relation analysis: application to the verification of reactive systems. Zbl 1067.68091
Jeannet, B.
7
2003
Infinite-state invariant checking with IC3 and predicate abstraction. Zbl 1368.68245
Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano
7
2016
Monitorability for the Hennessy-Milner logic with recursion. Zbl 1370.68203
Francalanza, Adrian; Aceto, Luca; Ingolfsdottir, Anna
7
2017
Scalable offline monitoring of temporal specifications. Zbl 1380.68268
Basin, David; Caronni, Germano; Ereth, Sarah; Harvan, Matúš; Klaedtke, Felix; Mantel, Heiko
7
2016
Some ways to reduce the space dimension in polyhedra computations. Zbl 1105.68107
Halbwachs, N.; Merchat, D.; Gonnord, L.
7
2006
Forest automata for verification of heap manipulation. Zbl 1284.68398
Habermehl, Peter; Holík, Lukáš; Rogalewicz, Adam; Šimáček, Jiří; Vojnar, Tomáš
7
2012
Automatic verification of competitive stochastic systems. Zbl 1291.68252
Chen, Taolue; Forejt, Vojtěch; Kwiatkowska, Marta; Parker, David; Simaitis, Aistis
7
2013
Model checking for probabilistic timed automata. Zbl 1291.68265
Norman, Gethin; Parker, David; Sproston, Jeremy
7
2013
Resolution proof transformation for compression and interpolation. Zbl 1317.68123
Rollini, Simone Fulvio; Bruttomesso, Roberto; Sharygina, Natasha; Tsitovich, Aliaksei
7
2014
Deciding floating-point logic with abstract conflict driven clause learning. Zbl 1317.68110
Brain, Martin; D’Silva, Vijay; Griggio, Alberto; Haller, Leopold; Kroening, Daniel
7
2014
A new heuristic for bad cycle detection using BDDs. Zbl 1001.68074
Hardin, R. H.; Kurshan, R. P.; Shukla, S. K.; Vardi, M. Y.
6
2001
Symbolic bounded synthesis. Zbl 1247.68163
Ehlers, Rüdiger
6
2012
BDD based procedures for a theory of equality with uninterpreted functions. Zbl 1021.68057
Goel, Anuj; Sajid, Khurram; Zhou, Hai; Aziz, Adnan; Singhal, Vigyan
6
2003
Compositional checking of satisfaction. Zbl 0776.68083
Andersen, Henrik Reif; Winskel, Glynn
6
1992
Distributed synthesis for well-connected architectures. Zbl 1180.68056
Gastin, Paul; Sznajder, Nathalie; Zeitoun, Marc
6
2009
Conformance testing for real-time systems. Zbl 1180.68072
Krichen, Moez; Tripakis, Stavros
6
2009
Hybrid systems: From verification to falsification by combining motion planning and discrete search. Zbl 1192.68692
Plaku, Erion; Kavraki, Lydia E.; Vardi, Moshe Y.
6
2009
Automatic symbolic compositional verification by learning assumptions. Zbl 1147.68052
Nam, Wonhong; Madhusudan, P.; Alur, Rajeev
6
2008
Code aware resource management. Zbl 1291.68137
Chatterjee, Krishnendu; De Alfaro, Luca; Faella, Marco; Majumdar, Rupak; Raman, Vishwanath
6
2013
A survey of partial-observation stochastic parity games. Zbl 1291.91022
Chatterjee, Krishnendu; Doyen, Laurent; Henzinger, Thomas A.
6
2013
Bayesian statistical model checking with application to Stateflow/Simulink verification. Zbl 1291.68273
Zuliani, Paolo; Platzer, André; Clarke, Edmund M.
6
2013
Finite controlled invariants for sampled switched systems. Zbl 1303.93121
Fribourg, L.; Kühne, U.; Soulat, R.
6
2014
Constructing the real numbers in HOL. Zbl 0809.68102
Harrison, John
6
1994
Pushdown module checking. Zbl 1209.68312
Bozzelli, Laura; Murano, Aniello; Peron, Adriano
6
2010
Modular and visual specification of hybrid systems: An introduction to HyCharts. Zbl 1018.68047
Grosu, Radu; Stauner, Thomas
5
2002
A scalable parallel algorithm for reachability analysis of very large circuits. Zbl 1020.68107
Heyman, Tamir; Geist, Danny; Grumberg, Orna; Schuster, Assaf
5
2002
From pre-historic to post-modern symbolic model checking. Zbl 1074.68036
Henzinger, Thomas A.; Kupferman, Orna; Qadeer, Shaz
5
2003
Static analysis for state-space reductions preserving temporal logics. Zbl 1073.68055
Yorav, Karen; Grumberg, Orna
5
2004
From LTL to deterministic automata. A safraless compositional approach. Zbl 1368.68233
Esparza, Javier; Křetínský, Jan; Sickert, Salomon
5
2016
A zonotopic framework for functional abstractions. Zbl 1331.68050
Goubault, Eric; Putot, Sylvie
5
2015
Local proofs for global safety properties. Zbl 1176.68118
Cohen, Ariel; Namjoshi, Kedar S.
5
2009
Computing differential invariants of hybrid systems as fixed points. Zbl 1180.93024
Platzer, André; Clarke, Edmund M.
5
2009
Timed verification of the generic architecture of a memory circuit using parametric timed automata. Zbl 1165.68401
Chevallier, Remy; Encrenaz-Tiphene, Emmanuelle; Fribourg, Laurent; Xu, Weiwen
5
2009
Model checking parameterized asynchronous shared-memory systems. Zbl 1360.68584
Durand-Gasselin, Antoine; Esparza, Javier; Ganty, Pierre; Majumdar, Rupak
5
2017
SMT-based scenario verification for hybrid systems. Zbl 1284.03216
Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano
5
2013
Weighted modal transition systems. Zbl 1291.68246
Bauer, Sebastian S.; Fahrenberg, Uli; Juhl, Line; Larsen, Kim G.; Legay, Axel; Thrane, Claus
5
2013
Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives. Zbl 1291.68251
Chatterjee, Krishnendu; Henzinger, Monika; Joglekar, Manas; Shah, Nisarg
5
2013
Quantitative monitoring of STL with edit distance. Zbl 1394.68230
Jakšić, Stefan; Bartocci, Ezio; Grosu, Radu; Nguyen, Thang; Ničković, Dejan
5
2018
From invariant checking to invariant inference using randomized search. Zbl 1358.68197
Sharma, Rahul; Aiken, Alex
5
2016
MSO logics for weighted timed automata. Zbl 1258.68089
Quaas, Karin
5
2011
Runtime enforcement monitors: Composition, synthesis, and enforcement abilities. Zbl 1219.68089
Falcone, Yliès; Mounier, Laurent; Fernandez, Jean-Claude; Richier, Jean-Luc
5
2011
Model checking for action-based logics. Zbl 0804.68086
Fantechi, Alessandro; Gnesi, Stefania; Ristori, Gioia
4
1994
Verification of a radio-based signaling system using the STATEMATE verification environment. Zbl 0990.68568
Damm, Werner; Klose, Jochen
4
2001
Relaxed visibility enhances partial order reduction. Zbl 0995.68060
Peled, Doron; Valmari, Antti; Kokkarinen, Ilkka
4
2001
Accelerating bounded model checking of safety properties. Zbl 1073.68054
Strichman, Ofer
4
2004
Experimental evaluation of verification and validation tools on Martian Rover software. Zbl 1078.68665
Brat, Guillaume; Drusinsky, Doron; Giannakopoulou, Dimitra; Goldberg, Allen; Havelund, Klaus; Lowry, Mike; Pasareanu, Corina; Venet, Arnaud; Visser, Willem; Washington, Rich
4
2004
Monitoring hyperproperties. Zbl 1425.68254
Finkbeiner, Bernd; Hahn, Christopher; Stenger, Marvin; Tentrup, Leander
2
2019
Some complexity results for stateful network verification. Zbl 1425.68248
Alpernas, Kalev; Panda, Aurojit; Rabinovich, Alexander; Sagiv, Mooly; Shenker, Scott; Shoham, Sharon; Velner, Yaron
1
2019
Probabilistic black-box reachability checking (extended version). Zbl 1425.68247
Aichernig, Bernhard K.; Tappler, Martin
1
2019
Almost event-rate independent monitoring. Zbl 1425.68249
Basin, David; Bhatt, Bhargav Nagaraja; Krstić, Srđan; Traytel, Dmitriy
1
2019
A survey of challenges for runtime verification from advanced application domains (beyond software). Zbl 1425.68268
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
1
2019
Quantitative monitoring of STL with edit distance. Zbl 1394.68230
Jakšić, Stefan; Bartocci, Ezio; Grosu, Radu; Nguyen, Thang; Ničković, Dejan
5
2018
Wireless protocol validation under uncertainty. Zbl 1394.68027
Shi, Jinghao; Lahiri, Shuvendu K.; Chandra, Ranveer; Challen, Geoffrey
2
2018
Solving parity games via priority promotion. Zbl 1390.68332
Benerecetti, Massimo; Dell’Erba, Daniele; Mogavero, Fabio
2
2018
On the complexity of monitoring Orchids signatures, and recurrence equations. Zbl 1394.68180
Goubault-Larrecq, Jean; Lachance, Jean-Philippe
1
2018
Finite-trace linear temporal logic: coinductive completeness. Zbl 1394.68237
Roşu, Grigore
1
2018
Enforcing termination of interprocedural analysis. Zbl 1425.68083
Schulze Frielinghaus, Stefan; Seidl, Helmut; Vogler, Ralf
1
2018
An improved algorithm for the control synthesis of nonlinear sampled switched systems. Zbl 1428.93053
Le Coënt, Adrien; dit Sandretto, Julien Alexandre; Chapoutot, Alexandre; Fribourg, Laurent
1
2018
Monitorability for the Hennessy-Milner logic with recursion. Zbl 1370.68203
Francalanza, Adrian; Aceto, Luca; Ingolfsdottir, Anna
7
2017
Model checking parameterized asynchronous shared-memory systems. Zbl 1360.68584
Durand-Gasselin, Antoine; Esparza, Javier; Ganty, Pierre; Majumdar, Rupak
5
2017
Percentile queries in multi-dimensional Markov decision processes. Zbl 1360.68518
Randour, Mickael; Raskin, Jean-François; Sankur, Ocan
4
2017
raSAT: an SMT solver for polynomial constraints. Zbl 1377.68140
Tung, Vu Xuan; Khanh, To Van; Ogawa, Mizuhito
3
2017
Solving quantified linear arithmetic by counterexample-guided instantiation. Zbl 1377.68138
Reynolds, Andrew; King, Tim; Kuncak, Viktor
3
2017
Propagation based local search for bit-precise reasoning. Zbl 1377.68134
Niemetz, Aina; Preiner, Mathias; Biere, Armin
3
2017
Robust online monitoring of signal temporal logic. Zbl 1370.68199
Deshmukh, Jyotirmoy V.; Donzé, Alexandre; Ghosh, Shromona; Jin, Xiaoqing; Juniwal, Garvit; Seshia, Sanjit A.
2
2017
Formal analysis and offline monitoring of electronic exams. Zbl 1370.68205
Kassem, Ali; Falcone, Yliès; Lafourcade, Pascal
2
2017
Predictive runtime enforcement. Zbl 1370.68207
Pinisetty, Srinivas; Preoteasa, Viorel; Tripakis, Stavros; Jéron, Thierry; Falcone, Yliès; Marchand, Hervé
2
2017
Empirical software metrics for benchmarking of verification tools. Zbl 1360.68371
Demyanova, Yulia; Pani, Thomas; Veith, Helmut; Zuleger, Florian
2
2017
Symbolic trajectory evaluation for word-level verification: theory and implementation. Zbl 1360.68582
Chakraborty, Supratik; Khasidashvili, Zurab; Seger, Carl-Johan H.; Gajavelly, Rajkumar; Haldankar, Tanmay; Chhatani, Dinesh; Mistry, Rakesh
2
2017
Collision avoidance for mobile robots with limited sensing and limited information about moving obstacles. Zbl 1370.68287
Phan, Dung; Yang, Junxing; Grosu, Radu; Smolka, Scott A.; Stoller, Scott D.
1
2017
Verifying data- and control-oriented properties combining static and runtime verification: theory and tools. Zbl 1370.68195
Ahrendt, Wolfgang; Chimento, Jesús Mauricio; Pace, Gordon J.; Schneider, Gerardo
1
2017
NP-completeness of small conflict set generation for congruence closure. Zbl 1377.68090
Fellner, Andreas; Fontaine, Pascal; Paleo, Bruno Woltzenlogel
1
2017
Cardinality constraints for arrays (decidability results and applications). Zbl 1377.68125
Alberti, F.; Ghilardi, S.; Pagani, E.
1
2017
\(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms. Zbl 1380.68279
Konnov, Igor; Lazić, Marijana; Veith, Helmut; Widder, Josef
1
2017
On compiling Boolean circuits optimized for secure multi-party computation. Zbl 1386.68020
Büscher, Niklas; Franz, Martin; Holzer, Andreas; Veith, Helmut; Katzenbeisser, Stefan
1
2017
Reachability computation for polynomial dynamical systems. Zbl 1360.93084
Dreossi, Tommaso; Dang, Thao; Piazza, Carla
1
2017
From non-preemptive to preemptive scheduling using synchronization synthesis. Zbl 1360.68346
Černý, Pavol; Clarke, Edmund M.; Henzinger, Thomas A.; Radhakrishna, Arjun; Ryzhyk, Leonid; Samanta, Roopsha; Tarrach, Thorsten
1
2017
Quantifying conformance using the Skorokhod metric. Zbl 1360.68629
Deshmukh, Jyotirmoy V.; Majumdar, Rupak; Prabhu, Vinayak S.
1
2017
SMT-based model checking for recursive programs. Zbl 1358.68072
Komuravelli, Anvesh; Gurfinkel, Arie; Chaki, Sagar
8
2016
Infinite-state invariant checking with IC3 and predicate abstraction. Zbl 1368.68245
Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano
7
2016
Scalable offline monitoring of temporal specifications. Zbl 1380.68268
Basin, David; Caronni, Germano; Ereth, Sarah; Harvan, Matúš; Klaedtke, Felix; Mantel, Heiko
7
2016
From LTL to deterministic automata. A safraless compositional approach. Zbl 1368.68233
Esparza, Javier; Křetínský, Jan; Sickert, Salomon
5
2016
From invariant checking to invariant inference using randomized search. Zbl 1358.68197
Sharma, Rahul; Aiken, Alex
5
2016
Organising LTL monitors over distributed systems with a global clock. Zbl 1380.68272
Colombo, Christian; Falcone, Yliès
3
2016
Decentralised LTL monitoring. Zbl 1392.68229
Bauer, Andreas; Falcone, Yliès
3
2016
A layered algorithm for quantifier elimination from linear modular constraints. Zbl 1368.68332
John, Ajith K.; Chakraborty, Supratik
2
2016
Synthesis of large dynamic concurrent programs from dynamic specifications. Zbl 1392.68143
Attie, Paul C.
2
2016
The spirit of ghost code. Zbl 1358.68070
Filliâtre, Jean-Christophe; Gondelman, Léon; Paskevich, Andrei
2
2016
Abstraction and mining of traces to explain concurrency bugs. Zbl 1380.68107
Tabaei Befrouei, Mitra; Wang, Chao; Weissenbacher, Georg
1
2016
ModelPlex: verified runtime validation of verified cyber-physical system models. Zbl 1380.68282
Mitsch, Stefan; Platzer, André
1
2016
Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components. Zbl 1404.68204
Wijs, Anton; Katoen, Joost-Pieter; Bošnački, Dragan
1
2016
Practical interruptible conversations: distributed dynamic verification with multiparty session types and Python. Zbl 1341.68118
Demangeon, Romain; Honda, Kohei; Hu, Raymond; Neykova, Rumyana; Yoshida, Nobuko
9
2015
Synthesising correct concurrent runtime monitors. Zbl 1323.68373
Francalanza, Adrian; Seychell, Aldrin
8
2015
A zonotopic framework for functional abstractions. Zbl 1331.68050
Goubault, Eric; Putot, Sylvie
5
2015
Generating models of infinite-state communication protocols using regular inference with abstraction. Zbl 1322.68131
Aarts, Fides; Jonsson, Bengt; Uijen, Johan; Vaandrager, Frits
4
2015
Under-approximating loops in C programs for fast counterexample detection. Zbl 1322.68054
Kroening, Daniel; Lewis, Matt; Weissenbacher, Georg
3
2015
Runtime verification with minimal intrusion through parallelism. Zbl 1323.68363
Berkovich, Shay; Bonakdarpour, Borzoo; Fischmeister, Sebastian
3
2015
On recursion-free Horn clauses and Craig interpolation. Zbl 1322.68134
Rümmer, Philipp; Hojjat, Hossein; Kuncak, Viktor
2
2015
Extended symbolic finite automata and transducers. Zbl 1341.68085
D’Antoni, Loris; Veanes, Margus
2
2015
Proving mutual termination. Zbl 1322.68052
Elenbogen, Dima; Katz, Shmuel; Strichman, Ofer
2
2015
Optimization techniques for Craig interpolant compaction in unbounded model checking. Zbl 1341.68117
Cabodi, Gianpiero; Loiacono, Carmelo; Vendraminetto, Danilo
2
2015
Evaluation of anonymity and confidentiality protocols using theorem proving. Zbl 1331.68028
Mhamdi, Tarek; Hasan, Osman; Tahar, Sofiène
1
2015
Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation). Zbl 1331.68048
Chaki, Sagar; Gurfinkel, Arie; Strichman, Ofer
1
2015
Program repair without regret. Zbl 1322.68056
von Essen, Christian; Jobstmann, Barbara
1
2015
Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists. Zbl 1322.68121
Garg, Pranav; Löding, Christof; Madhusudan, P.; Neider, Daniel
1
2015
Monitoring of temporal first-order properties with aggregations. Zbl 1323.68362
Basin, David; Klaedtke, Felix; Marinovic, Srdjan; Zălinescu, Eugen
1
2015
Hybrid automata-based CEGAR for rectangular hybrid systems. Zbl 1341.68109
Prabhakar, Pavithra; Duggirala, Parasara Sridhar; Mitra, Sayan; Viswanathan, Mahesh
1
2015
A game approach to determinize timed automata. Zbl 1323.68337
Bertrand, Nathalie; Stainer, Amélie; Jéron, Thierry; Krichen, Moez
1
2015
Resolution proof transformation for compression and interpolation. Zbl 1317.68123
Rollini, Simone Fulvio; Bruttomesso, Roberto; Sharygina, Natasha; Tsitovich, Aliaksei
7
2014
Deciding floating-point logic with abstract conflict driven clause learning. Zbl 1317.68110
Brain, Martin; D’Silva, Vijay; Griggio, Alberto; Haller, Leopold; Kroening, Daniel
7
2014
Finite controlled invariants for sampled switched systems. Zbl 1303.93121
Fribourg, L.; Kühne, U.; Soulat, R.
6
2014
An extension of lazy abstraction with interpolation for programs with arrays. Zbl 1317.68107
Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha
4
2014
Budget-bounded model-checking pushdown systems. Zbl 1317.68106
Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Rezine, Othmane; Stenman, Jari
4
2014
Runtime enforcement of timed properties revisited. Zbl 1314.68102
Pinisetty, Srinivas; Falcone, Yliès; Jéron, Thierry; Marchand, Hervé; Rollet, Antoine; Nguena Timo, Omer
4
2014
QoS-aware management of monotonic service orchestrations. Zbl 1291.68280
Benveniste, Albert; Jard, Claude; Kattepur, Ajay; Rosario, Sidney; Thywissen, John A.
2
2014
Automata-based symbolic string analysis for vulnerability detection. Zbl 1291.68272
Yu, Fang; Alkhalaf, Muath; Bultan, Tevfik; Ibarra, Oscar H.
2
2014
Runtime verification of embedded real-time systems. Zbl 1317.68122
Reinbacher, Thomas; Függer, Matthias; Brauer, Jörg
2
2014
Quantifier elimination by dependency sequents. Zbl 1311.03061
Goldberg, Eugene; Manolios, Panagiotis
2
2014
An abstraction-refinement framework for trigger querying. Zbl 1291.68242
Avni, Guy; Kupferman, Orna
1
2014
Model checking approach to automated planning. Zbl 1291.68263
Li, Yi; Dong, Jin Song; Sun, Jing; Liu, Yang; Sun, Jun
1
2014
A modal characterization of alternating approximate bisimilarity. Zbl 1300.93114
Zhang, Jinjin; Zhu, Zhaohui
1
2014
Hardness and inapproximability of minimizing adaptive distinguishing sequences. Zbl 1317.68125
Türker, Uraz Cengiz; Yenigün, Hüsnü
1
2014
Quantifier-free encoding of invariants for hybrid systems. Zbl 1317.68111
Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano
1
2014
Efficiently solving quantified bit-vector formulas. Zbl 1284.03212
Wintersteiger, Christoph M.; Hamadi, Youssef; De Moura, Leonardo
16
2013
A compositional modelling and analysis framework for stochastic hybrid systems. Zbl 1291.68293
Hahn, Ernst Moritz; Hartmanns, Arnd; Hermanns, Holger; Katoen, Joost-Pieter
11
2013
Computable fixpoints in well-structured symbolic model checking. Zbl 1291.68247
Bertrand, N.; Schnoebelen, P.
10
2013
Automatic verification of competitive stochastic systems. Zbl 1291.68252
Chen, Taolue; Forejt, Vojtěch; Kwiatkowska, Marta; Parker, David; Simaitis, Aistis
7
2013
Model checking for probabilistic timed automata. Zbl 1291.68265
Norman, Gethin; Parker, David; Sproston, Jeremy
7
2013
Code aware resource management. Zbl 1291.68137
Chatterjee, Krishnendu; De Alfaro, Luca; Faella, Marco; Majumdar, Rupak; Raman, Vishwanath
6
2013
A survey of partial-observation stochastic parity games. Zbl 1291.91022
Chatterjee, Krishnendu; Doyen, Laurent; Henzinger, Thomas A.
6
2013
Bayesian statistical model checking with application to Stateflow/Simulink verification. Zbl 1291.68273
Zuliani, Paolo; Platzer, André; Clarke, Edmund M.
6
2013
SMT-based scenario verification for hybrid systems. Zbl 1284.03216
Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano
5
2013
Weighted modal transition systems. Zbl 1291.68246
Bauer, Sebastian S.; Fahrenberg, Uli; Juhl, Line; Larsen, Kim G.; Legay, Axel; Thrane, Claus
5
2013
Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives. Zbl 1291.68251
Chatterjee, Krishnendu; Henzinger, Monika; Joglekar, Manas; Shah, Nisarg
5
2013
SMT proof checking using a logical framework. Zbl 1284.68521
Stump, Aaron; Oe, Duckki; Reynolds, Andrew; Hadarean, Liana; Tinelli, Cesare
4
2013
Ranking function synthesis for bit-vector relations. Zbl 1291.68138
Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M.
4
2013
Analyzing probabilistic pushdown automata. Zbl 1291.68226
Brázdil, Tomáš; Esparza, Javier; Kiefer, Stefan; Kučera, Antonín
4
2013
An extension of the inverse method to probabilistic timed automata. Zbl 1291.68240
André, Étienne; Fribourg, Laurent; Sproston, Jeremy
3
2013
On-the-fly verification and optimization of DTA-properties for large Markov chains. Zbl 1291.68295
Mikeev, Linar; Neuhäußer, Martin R.; Spieler, David; Wolf, Verena
3
2013
Beyond vacuity: towards the strongest passing formula. Zbl 1291.68253
Chockler, Hana; Gurfinkel, Arie; Strichman, Ofer
3
2013
Loop summarization using state and transition invariants. Zbl 1291.68262
Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M.
2
2013
Algorithmic probabilistic game semantics. Playing games with automata. Zbl 1291.68294
Kiefer, Stefan; Murawski, Andrzej S.; Ouaknine, Joël; Wachter, Björn; Worrell, James
2
2013
Being careful about theory combination. Zbl 1284.68518
Jovanović, Dejan; Barrett, Clark
1
2013
Time-triggered runtime verification. Zbl 1291.68248
Bonakdarpour, Borzoo; Navabpour, Samaneh; Fischmeister, Sebastian
1
2013
Composition of password-based protocols. Zbl 1291.68035
Chevalier, Céline; Delaune, Stéphanie; Kremer, Steve; Ryan, Mark D.
1
2013
Applying string-rewriting to sequence-based specification. Zbl 1291.68255
Eschbach, Robert; Lin, Lan; Poore, Jesse H.
1
2013
...and 208 more Documents
all top 5

Cited by 1,998 Authors

22 Chatterjee, Krishnendu
18 Kröning, Daniel
16 Kwiatkowska, Marta Z.
15 Meseguer Guaita, José
14 Kupferman, Orna
14 Larsen, Kim Guldstrand
14 Markey, Nicolas
14 Raskin, Jean-François
13 Falcone, Yliès
12 Bouyer, Patricia
12 Legay, Axel
12 Norman, Gethin
12 Vardi, Moshe Y.
11 Abdulla, Parosh Aziz
10 Basin, David A.
10 Francalanza, Adrian
10 Grumberg, Orna
10 Zimmermann, Martín G.
9 Baier, Christel
9 Sharygina, Natasha
8 Aceto, Luca
8 Bloem, Roderick
8 Doyen, Laurent
8 Fahrenberg, Uli
8 Finkel, Alain
8 Henzinger, Thomas A.
8 Lime, Didier
8 Peled, Doron A.
7 André, Étienne
7 Baldan, Paolo
7 Beyersdorff, Olaf
7 Biere, Armin
7 Cimatti, Alessandro
7 Fribourg, Laurent
7 Haddad, Serge
7 Jobstmann, Barbara
7 King, Andy
7 Klaedtke, Felix
7 Marchand, Hervé
7 Murano, Aniello
7 Olveczky, Peter Csaba
7 Pnueli, Amir
7 Rümmer, Philipp
7 Tonetta, Stefano
6 Barrett, Clark W.
6 Bensalem, Saddek
6 Bérard, Béatrice
6 Bertrand, Nathalie
6 Bollig, Beate
6 Bonakdarpour, Borzoo
6 Donaldson, Alastair F.
6 Ingólfsdóttir, Anna
6 Jéron, Thierry
6 Jonsson, Bengt
6 Katoen, Joost-Pieter
6 Khomenko, Victor
6 Kulkarni, Sandeep S.
6 La Torre, Salvatore
6 Lafortune, Stéphane
6 Lange, Martin
6 Li, Yongming
6 Mateescu, Radu
6 Roşu, Grigore
6 Roux, Olivier H.
6 Strichman, Ofer
6 Subramani, Krishnan
6 Tripakis, Stavros
6 Walukiewicz, Igor
6 Wintersteiger, Christoph M.
6 Zhang, Lijun
5 Bartocci, Ezio
5 Beneš, Nikola
5 Bliudze, Simon
5 Bozzelli, Laura
5 Brauer, Jörg
5 Brihaye, Thomas
5 Brim, Luboš
5 Chockler, Hana
5 Clarke, Edmund Melson jun.
5 Droste, Manfred
5 D’silva, Vijay
5 Fokkink, Willem Jan
5 Forejt, Vojtěch
5 Garavel, Hubert
5 Gastin, Paul
5 Geeraerts, Gilles
5 Goubault-Larrecq, Jean
5 Heule, Marijn J. H.
5 Janota, Mikoláš
5 Konnov, Igor V.
5 Koutny, Maciej
5 Křetínský, Jan
5 Majumdar, Rupak
5 Movaghar, Ali
5 Muscholl, Anca
5 Quaas, Karin
5 Randour, Mickael
5 Rauch Henzinger, Monika
5 Reynolds, Andrew
5 Schnoebelen, Philippe
...and 1,898 more Authors
all top 5

Cited in 105 Journals

168 Formal Methods in System Design
124 Theoretical Computer Science
61 Information and Computation
53 Formal Aspects of Computing
41 Journal of Automated Reasoning
40 Acta Informatica
23 Journal of Logical and Algebraic Methods in Programming
20 Journal of Computer and System Sciences
19 Logical Methods in Computer Science
17 Information Processing Letters
16 Science of Computer Programming
16 The Journal of Logic and Algebraic Programming
15 Discrete Event Dynamic Systems
13 Automatica
13 International Journal of Foundations of Computer Science
10 Nonlinear Analysis. Hybrid Systems
9 Artificial Intelligence
9 Programming and Computer Software
9 Annals of Mathematics and Artificial Intelligence
7 Real-Time Systems
6 Distributed Computing
6 Mathematical Problems in Engineering
6 RAIRO. Theoretical Informatics and Applications
6 Journal of Applied Logic
5 MSCS. Mathematical Structures in Computer Science
5 Fundamenta Informaticae
5 Journal of Applied Mathematics
5 ACM Transactions on Computational Logic
4 Journal of Computer Science and Technology
4 Algorithmica
4 Constraints
4 Theory of Computing Systems
4 Higher-Order and Symbolic Computation
4 Computer Languages, Systems & Structures
4 Algorithms
3 Discrete Applied Mathematics
3 Fuzzy Sets and Systems
3 Systems & Control Letters
3 Journal of Symbolic Computation
3 International Journal of Approximate Reasoning
3 The Bulletin of Symbolic Logic
3 Journal of the ACM
3 Theory and Practice of Logic Programming
2 International Journal of Control
2 International Journal of General Systems
2 Information Sciences
2 Studia Logica
2 International Journal of Parallel Programming
2 Journal of Parallel and Distributed Computing
2 Journal of Logic, Language and Information
2 Journal of Computer and Systems Sciences International
2 Journal of Functional Programming
2 European Journal of Control
2 Soft Computing
2 Mathematics in Computer Science
2 Science China. Information Sciences
2 Frontiers of Computer Science
2 Computer Science Review
1 ACM Computing Surveys
1 International Journal of Theoretical Physics
1 Linear and Multilinear Algebra
1 Rocky Mountain Journal of Mathematics
1 Computing
1 Journal of Optimization Theory and Applications
1 Mathematics and Computers in Simulation
1 SIAM Journal on Computing
1 Software. Practice & Experience
1 Synthese
1 Annals of Pure and Applied Logic
1 Asia-Pacific Journal of Operational Research
1 Journal of Cryptology
1 Random Structures & Algorithms
1 Neural Computation
1 Computational Geometry
1 International Journal of Algebra and Computation
1 Numerical Algorithms
1 Automation and Remote Control
1 Journal of Statistical Computation and Simulation
1 Linear Algebra and its Applications
1 International Journal of Robust and Nonlinear Control
1 Advances in Engineering Software
1 Cybernetics and Systems Analysis
1 Journal of Applied Non-Classical Logics
1 The Journal of Artificial Intelligence Research (JAIR)
1 International Transactions in Operational Research
1 Science in China. Series E
1 Journal of Combinatorial Optimization
1 Journal of Applied Mathematics and Decision Sciences
1 Discrete Dynamics in Nature and Society
1 LMS Journal of Computation and Mathematics
1 Journal of Systems Science and Complexity
1 ACM Journal of Experimental Algorithmics
1 International Journal of Quantum Information
1 Discrete Optimization
1 Sibirskie Èlektronnye Matematicheskie Izvestiya
1 Science in China. Series F
1 Proceedings of the Steklov Institute of Mathematics
1 Mathematical Modelling of Natural Phenomena
1 Acta Universitatis Sapientiae. Informatica
1 The Review of Symbolic Logic
...and 5 more Journals

Citations by Year