Journal: Formal Methods in System Design

Volume 45, Issue 3

303 -- 329Laurent Fribourg, Ulrich Kühne, Romain Soulat. Finite controlled invariants for sampled switched systems
330 -- 380Gilles Geeraerts, Jean-François Raskin, Nathalie Sznajder. On regions and zones for event-clock automata
381 -- 422Srinivas Pinisetty, Yliès Falcone, Thierry Jéron, Hervé Marchand, Antoine Rollet, Omer Nguena-Timo. Runtime enforcement of timed properties revisited

Volume 45, Issue 2

111 -- 143Eugene Goldberg, Panagiotis Manolios. Quantifier elimination by dependency sequents
144 -- 164Jiazhao Xu, Mark Williams, Hari Mony, Jason Baumgartner. Scalable reachability analysis via automated dynamic netlist-based hint generation
165 -- 188Alessandro Cimatti, Sergio Mover, Stefano Tonetta. Quantifier-free encoding of invariants for hybrid systems
189 -- 212Alexey Lvov, Luis Alfonso Lastras-Montaño, Barry M. Trager, Viresh Paruthi, Robert Shadowen, Ali El-Zein. Verification of Galois field based circuits by formal reasoning based on computational algebraic geometry
213 -- 245Martin Brain, Vijay D'Silva, Alberto Griggio, Leopold Haller, Daniel Kroening. Deciding floating-point logic with abstract conflict driven clause learning
246 -- 272Chao Yan, Mark R. Greenstreet, Suwen Yang. Verifying global start-up for a Möbius ring-oscillator
273 -- 301Parosh Aziz Abdulla, Mohamed Faouzi Atig, Othmane Rezine, Jari Stenman. Budget-bounded model-checking pushdown systems

Volume 45, Issue 1

1 -- 41Simone Fulvio Rollini, Roberto Bruttomesso, Natasha Sharygina, Aliaksei Tsitovich. Resolution proof transformation for compression and interpolation
42 -- 62Dingbao Xie, Lei Bu, Jianhua Zhao, Xuandong Li. SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata
63 -- 109Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina. An extension of lazy abstraction with interpolation for programs with arrays