Journal: Formal Methods in System Design

Volume 51, Issue 3

431 -- 432Alberto Griggio, Philipp Rümmer. Preface to special issue on satisfiability modulo theories
433 -- 461Martin Bromberger, Christoph Weidenbach. New techniques for linear arithmetic: cubes and equalities
462 -- 499Vu Xuan Tung, To Van Khanh, Mizuhito Ogawa. raSAT: an SMT solver for polynomial constraints
500 -- 532Andrew Reynolds, Tim King 0001, Viktor Kuncak. Solving quantified linear arithmetic by counterexample-guided instantiation
533 -- 544Andreas Fellner, Pascal Fontaine, Bruno Woltzenlogel Paleo. NP-completeness of small conflict set generation for congruence closure
545 -- 574Francesco Alberti, Silvio Ghilardi, Elena Pagani. Cardinality constraints for arrays (decidability results and applications)
575 -- 607Constantin Enea, Ondrej Lengál, Mihaela Sighireanu, Tomás Vojnar. Compositional entailment checking for a fragment of separation logic
608 -- 636Aina Niemetz, Mathias Preiner, Armin Biere. Propagation based local search for bit-precise reasoning

Volume 51, Issue 2

267 -- 269Georg Gottlob, Thomas A. Henzinger, Georg Weissenbacher. Preface of the Special Issue in Memoriam Helmut Veith
270 -- 307Igor Konnov, Marijana Lazic, Helmut Veith, Josef Widder. 2: parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
308 -- 331Niklas Büscher, Martin Franz, Andreas Holzer, Helmut Veith, Stefan Katzenbeisser 0001. On compiling Boolean circuits optimized for secure multi-party computation
332 -- 361Bettina Könighofer, Mohammed Alshiekh, Roderick Bloem, Laura Humphrey, Robert Könighofer, Ufuk Topcu, Chao Wang. Shield synthesis
362 -- 394William R. Harris, Somesh Jha, Thomas W. Reps, Sanjit A. Seshia. Program synthesis for interactive-security systems
395 -- 418Frederic Doucet, Robert Kurshan. A methodology to take credit for high-level verification during RTL verification
419 -- 430Johann A. Makowsky, Anna Zamansky. Keeping logic in the trivium of computer science: a teaching perspective

Volume 51, Issue 1

1 -- 4Ezio Bartocci, Rupak Majumdar. Introduction to the special issue on runtime verification
5 -- 30Jyotirmoy V. Deshmukh, Alexandre Donzé, Shromona Ghosh, Xiaoqing Jin, Garvit Juniwal, Sanjit A. Seshia. Robust online monitoring of signal temporal logic
31 -- 61Patrick Moosbrugger, Kristin Y. Rozier, Johann Schumann. R2U2: monitoring and diagnosis of security threats for unmanned aerial systems
62 -- 86Dung Phan, Junxing Yang, Radu Grosu, Scott A. Smolka, Scott D. Stoller. Collision avoidance for mobile robots with limited sensing and limited information about moving obstacles
87 -- 116Adrian Francalanza, Luca Aceto, Anna Ingólfsdóttir. Monitorability for the Hennessy-Milner logic with recursion
117 -- 153Ali Kassem 0001, Yliès Falcone, Pascal Lafourcade 0001. Formal analysis and offline monitoring of electronic exams
154 -- 199Srinivas Pinisetty, Viorel Preoteasa, Stavros Tripakis, Thierry Jéron, Yliès Falcone, Hervé Marchand. Predictive runtime enforcement
200 -- 265Wolfgang Ahrendt, Jesús Mauricio Chimento, Gordon J. Pace, Gerardo Schneider. Verifying data- and control-oriented properties combining static and runtime verification: theory and tools