Exibard, Léo; Filiot, Emmanuel; Khalimov, Ayrat Church synthesis on register automata over linearly ordered data domains. (English) Zbl 07815091 Form. Methods Syst. Des. 61, No. 2-3, 290-337 (2022). MSC: 68-XX PDFBibTeX XMLCite \textit{L. Exibard} et al., Form. Methods Syst. Des. 61, No. 2--3, 290--337 (2022; Zbl 07815091) Full Text: DOI arXiv
Bresolin, Davide; El-Fakih, Khaled; Villa, Tiziano; Yevtushenko, Nina Equivalence checking and intersection of deterministic timed finite state machines. (English) Zbl 1522.68260 Form. Methods Syst. Des. 59, No. 1-3, 77-102 (2021). MSC: 68Q45 PDFBibTeX XMLCite \textit{D. Bresolin} et al., Form. Methods Syst. Des. 59, No. 1--3, 77--102 (2021; Zbl 1522.68260) Full Text: DOI arXiv
Alur, Rajeev; Fisman, Dana Colored nested words. (English) Zbl 1492.68076 Form. Methods Syst. Des. 58, No. 3, 347-374 (2021). MSC: 68Q45 68N30 68Q42 68Q60 PDFBibTeX XMLCite \textit{R. Alur} and \textit{D. Fisman}, Form. Methods Syst. Des. 58, No. 3, 347--374 (2021; Zbl 1492.68076) Full Text: DOI
Jančík, Pavel; Kofroň, Jan; Alt, Leonardo; Fedyukovich, Grigory; Hyvärinen, Antti E. J.; Sharygina, Natasha Exploiting partial variable assignment in interpolation-based model checking. (English) Zbl 1425.68257 Form. Methods Syst. Des. 55, No. 1, 33-71 (2019). MSC: 68Q60 03C40 68T20 PDFBibTeX XMLCite \textit{P. Jančík} et al., Form. Methods Syst. Des. 55, No. 1, 33--71 (2019; Zbl 1425.68257) Full Text: DOI
Bollig, Benedikt; Grindei, Manuela-Lidia; Habermehl, Peter Realizability of concurrent recursive programs. (English) Zbl 1425.68062 Form. Methods Syst. Des. 53, No. 3, 339-362 (2018). MSC: 68N30 68Q45 68Q60 68Q85 PDFBibTeX XMLCite \textit{B. Bollig} et al., Form. Methods Syst. Des. 53, No. 3, 339--362 (2018; Zbl 1425.68062) 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
Harris, William R.; Jha, Somesh; Reps, Thomas W.; Seshia, Sanjit A. Program synthesis for interactive-security systems. (English) Zbl 1386.68032 Form. Methods Syst. Des. 51, No. 2, 362-394 (2017). MSC: 68N30 PDFBibTeX XMLCite \textit{W. R. Harris} et al., Form. Methods Syst. Des. 51, No. 2, 362--394 (2017; Zbl 1386.68032) Full Text: DOI Link
Sharma, Rahul; Aiken, Alex From invariant checking to invariant inference using randomized search. (English) Zbl 1358.68197 Form. Methods Syst. Des. 48, No. 3, 235-256 (2016). MSC: 68Q60 68P05 68T20 PDFBibTeX XMLCite \textit{R. Sharma} and \textit{A. Aiken}, Form. Methods Syst. Des. 48, No. 3, 235--256 (2016; Zbl 1358.68197) Full Text: DOI
Attie, Paul C. Synthesis of large dynamic concurrent programs from dynamic specifications. (English) Zbl 1392.68143 Form. Methods Syst. Des. 48, No. 1-2, 94-147 (2016). MSC: 68N30 68Q60 68Q85 PDFBibTeX XMLCite \textit{P. C. Attie}, Form. Methods Syst. Des. 48, No. 1--2, 94--147 (2016; Zbl 1392.68143) Full Text: DOI arXiv
Heinen, Jonathan; Jansen, Christina; Katoen, Joost-Pieter; Noll, Thomas Juggrnaut: using graph grammars for abstracting unbounded heap structures. (English) Zbl 1341.68033 Form. Methods Syst. Des. 47, No. 2, 159-203 (2015). MSC: 68P05 68N30 68Q42 PDFBibTeX XMLCite \textit{J. Heinen} et al., Form. Methods Syst. Des. 47, No. 2, 159--203 (2015; Zbl 1341.68033) Full Text: DOI
Garg, Pranav; Löding, Christof; Madhusudan, P.; Neider, Daniel Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists. (English) Zbl 1322.68121 Form. Methods Syst. Des. 47, No. 1, 120-157 (2015). MSC: 68Q45 68P05 68Q32 PDFBibTeX XMLCite \textit{P. Garg} et al., Form. Methods Syst. Des. 47, No. 1, 120--157 (2015; Zbl 1322.68121) Full Text: DOI
Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Rezine, Othmane; Stenman, Jari Budget-bounded model-checking pushdown systems. (English) Zbl 1317.68106 Form. Methods Syst. Des. 45, No. 2, 273-301 (2014). MSC: 68Q60 68Q85 68Q25 68Q45 PDFBibTeX XMLCite \textit{P. A. Abdulla} et al., Form. Methods Syst. Des. 45, No. 2, 273--301 (2014; Zbl 1317.68106) Full Text: DOI
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
Habermehl, Peter; Holík, Lukáš; Rogalewicz, Adam; Šimáček, Jiří; Vojnar, Tomáš Forest automata for verification of heap manipulation. (English) Zbl 1284.68398 Form. Methods Syst. Des. 41, No. 1, 83-106 (2012). MSC: 68Q60 68Q45 68P05 PDFBibTeX XMLCite \textit{P. Habermehl} et al., Form. Methods Syst. Des. 41, No. 1, 83--106 (2012; Zbl 1284.68398) Full Text: DOI
Ehlers, Rüdiger Symbolic bounded synthesis. (English) Zbl 1247.68163 Form. Methods Syst. Des. 40, No. 2, 232-262 (2012). MSC: 68Q60 03B70 PDFBibTeX XMLCite \textit{R. Ehlers}, Form. Methods Syst. Des. 40, No. 2, 232--262 (2012; Zbl 1247.68163) 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
Quaas, Karin MSO logics for weighted timed automata. (English) Zbl 1258.68089 Form. Methods Syst. Des. 38, No. 3, 193-222 (2011). MSC: 68Q45 03D05 PDFBibTeX XMLCite \textit{K. Quaas}, Form. Methods Syst. Des. 38, No. 3, 193--222 (2011; Zbl 1258.68089) Full Text: DOI
Bozzelli, Laura; Murano, Aniello; Peron, Adriano Pushdown module checking. (English) Zbl 1209.68312 Form. Methods Syst. Des. 36, No. 1, 65-95 (2010). MSC: 68Q60 PDFBibTeX XMLCite \textit{L. Bozzelli} et al., Form. Methods Syst. Des. 36, No. 1, 65--95 (2010; Zbl 1209.68312) Full Text: DOI
Cook, Byron; Podelski, Andreas; Rybalchenko, Andrey Summarization for termination: No return! (English) Zbl 1185.68412 Form. Methods Syst. Des. 35, No. 3, 369-387 (2009). MSC: 68Q60 PDFBibTeX XMLCite \textit{B. Cook} et al., Form. Methods Syst. Des. 35, No. 3, 369--387 (2009; Zbl 1185.68412) Full Text: DOI
Bozzelli, Laura; La Torre, Salvatore Decision problems for lower/upper bound parametric timed automata. (English) Zbl 1186.68245 Form. Methods Syst. Des. 35, No. 2, 121-151 (2009). MSC: 68Q45 68Q60 PDFBibTeX XMLCite \textit{L. Bozzelli} and \textit{S. La Torre}, Form. Methods Syst. Des. 35, No. 2, 121--151 (2009; Zbl 1186.68245) Full Text: DOI
Gastin, Paul; Sznajder, Nathalie; Zeitoun, Marc Distributed synthesis for well-connected architectures. (English) Zbl 1180.68056 Form. Methods Syst. Des. 34, No. 3, 215-237 (2009). MSC: 68M14 68Q60 PDFBibTeX XMLCite \textit{P. Gastin} et al., Form. Methods Syst. Des. 34, No. 3, 215--237 (2009; Zbl 1180.68056) 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
Nam, Wonhong; Madhusudan, P.; Alur, Rajeev Automatic symbolic compositional verification by learning assumptions. (English) Zbl 1147.68052 Form. Methods Syst. Des. 32, No. 3, 207-234 (2008). MSC: 68Q60 68Q32 68Q45 PDFBibTeX XMLCite \textit{W. Nam} et al., Form. Methods Syst. Des. 32, No. 3, 207--234 (2008; Zbl 1147.68052) Full Text: DOI
Chaki, Sagar; Clarke, Edmund; Sharygina, Natasha; Sinha, Nishant Verification of evolving software via component substitutability analysis. (English) Zbl 1147.68047 Form. Methods Syst. Des. 32, No. 3, 235-266 (2008). MSC: 68Q60 68N30 PDFBibTeX XMLCite \textit{S. Chaki} et al., Form. Methods Syst. Des. 32, No. 3, 235--266 (2008; Zbl 1147.68047) Full Text: DOI Link
Gupta, Anubhav; McMillan, K. L.; Fu, Zhaohui Automated assumption generation for compositional verification. (English) Zbl 1147.68050 Form. Methods Syst. Des. 32, No. 3, 285-301 (2008). MSC: 68Q60 PDFBibTeX XMLCite \textit{A. Gupta} et al., Form. Methods Syst. Des. 32, No. 3, 285--301 (2008; Zbl 1147.68050) Full Text: DOI
Păsăreanu, Corina S.; Giannakopoulou, Dimitra; Bobaru, Mihaela Gheorghiu; Cobleigh, Jamieson M.; Barringer, Howard Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning. (English) Zbl 1147.68053 Form. Methods Syst. Des. 32, No. 3, 175-205 (2008). MSC: 68Q60 68Q32 PDFBibTeX XMLCite \textit{C. S. Păsăreanu} et al., Form. Methods Syst. Des. 32, No. 3, 175--205 (2008; Zbl 1147.68053) Full Text: DOI
Chaki, Sagar; Strichman, Ofer Three optimizations for assume-guarantee reasoning with \(L^{*}\). (English) Zbl 1147.68569 Form. Methods Syst. Des. 32, No. 3, 267-284 (2008). MSC: 68Q60 68Q85 68Q32 PDFBibTeX XMLCite \textit{S. Chaki} and \textit{O. Strichman}, Form. Methods Syst. Des. 32, No. 3, 267--284 (2008; Zbl 1147.68569) Full Text: DOI
Bouyer, Patricia; Brinksma, Ed; Larsen, Kim G. Optimal infinite scheduling for multi-priced timed automata. (English) Zbl 1133.68360 Form. Methods Syst. Des. 32, No. 1, 3-23 (2008). MSC: 68Q45 90B35 PDFBibTeX XMLCite \textit{P. Bouyer} et al., Form. Methods Syst. Des. 32, No. 1, 3--23 (2008; Zbl 1133.68360) Full Text: DOI
La Torre, Salvatore; Napoli, Margherita; Parente, Mimmo The word problem for visibly pushdown languages described by grammars. (English) Zbl 1131.68053 Form. Methods Syst. Des. 31, No. 3, 265-279 (2007). MSC: 68Q45 03D40 68Q60 PDFBibTeX XMLCite \textit{S. La Torre} et al., Form. Methods Syst. Des. 31, No. 3, 265--279 (2007; Zbl 1131.68053) Full Text: DOI
Bouyer, Patricia; Brihaye, Thomas; Bruyère, Véronique; Raskin, Jean-François On the optimal reachability problem of weighted timed automata. (English) Zbl 1129.68039 Form. Methods Syst. Des. 31, No. 2, 135-175 (2007). MSC: 68Q45 PDFBibTeX XMLCite \textit{P. Bouyer} et al., Form. Methods Syst. Des. 31, No. 2, 135--175 (2007; Zbl 1129.68039) Full Text: DOI Link
Vardhan, Abhay; Viswanathan, Mahesh Learning to verify branching time properties. (English) Zbl 1118.68554 Form. Methods Syst. Des. 31, No. 1, 35-61 (2007). MSC: 68Q60 PDFBibTeX XMLCite \textit{A. Vardhan} and \textit{M. Viswanathan}, Form. Methods Syst. Des. 31, No. 1, 35--61 (2007; Zbl 1118.68554) Full Text: DOI Link