×

FOCI

swMATH ID: 12868
Software Authors: Ranjit Jhala, Kenneth L. McMillan
Description: FOCI: and interpolating prover. FOCI is a decision procedure for quantifier-free first-order formulas. It supports certain interpreted theories, such as equality, uninterpreted functions, linear arithmetic, and arrays. Most importantly, it can compute quantifier-free Craig interpolants for inconsistent pairs (or more generally, sequences) of formulas. This has a number of applications in infinite-state verification, for example, discovering predicates in predicate abstraction, and computing inductive invariants.
Homepage: http://www.kenmcmil.com/foci.html
Related Software: Princess; z3; CSIsat; SIMPLIFY; Chaff; BLAST; Yices; MiniSat; OpenSMT; SMT-LIB; MathSAT5; Wolverine; CVC4; SatAbs; SPIN; SATO; MathSAT; VAMPIRE; GitHub; Bebop
Referenced in: 63 Publications
all top 5

Referenced by 106 Authors

5 McMillan, Kenneth L.
4 Bruttomesso, Roberto
4 Griggio, Alberto
4 Kröning, Daniel
4 Rümmer, Philipp
4 Sebastiani, Roberto
4 Sofronie-Stokkermans, Viorica
4 Tinelli, Cesare
3 Bonacina, Maria Paola
3 Ghilardi, Silvio
3 Goel, Amit
3 Johansson, Moa
3 Krstic, Sava A.
3 Ranise, Silvio
3 Song, Xiaoyu
2 Brillout, Angelo
2 Chen, Mingshuai
2 Cimatti, Alessandro
2 Dutertre, Bruno
2 Fuchs, Alexander
2 Grundy, Jim
2 Gu, Ming
2 Jung, Yungbum
2 Kemper, Stephanie
2 Kupferschmid, Stefan
2 Le, Thi Thieu Hoa
2 Lee, Wonchan
2 Li, Li
2 Rasga, João
2 Rybalchenko, Andrey
2 Sernadas, Amilcar C.
2 Sernadas, Cristina S.
2 Tang, Yuefeng
2 Wahl, Thomas
2 Wang, Bow-Yaw
2 Yi, Kwangkeun
1 Abdulla, Parosh Aziz
1 Backeman, Peter
1 Barrett, Clark W.
1 Batz, Kevin
1 Becker, Bernd
1 Biere, Armin
1 Chen, Yu-Fang
1 Cheng, Xi
1 Christ, Jürgen
1 Clarke, Edmund Melson jun.
1 Dai, Liyun
1 de Moura, Leonardo
1 Delzanno, Giorgio
1 Eggers, Andreas
1 Esen, Zafer
1 Gaĭnă, Daniel
1 Gan, Ting
1 Gange, Graeme
1 Grumberg, Orna
1 Guo, Lei
1 Gupta, Ashutosh
1 Haziza, Frédéric
1 He, Kai-Duo
1 Hoenicke, Jochen
1 Hong, Chih-Duo
1 Jain, Himanshu
1 Jhala, Ranjit
1 Jovanović, Dejan
1 Kalinnik, Natalia
1 Kaminski, Benjamin Lucien
1 Kapur, Deepak
1 Katoen, Joost-Pieter
1 Kovács, Laura Ildikó
1 Lin, HongZhi
1 Luo, Xiangyu
1 Majumdar, Rupak
1 Mandrykin, M. U.
1 Matheja, Christoph
1 Monniaux, David P.
1 Mutilin, V. S.
1 Navas, Jorge A.
1 Popescu, Andrei
1 Renardel de Lavalette, Gerard R.
1 Rezine, Ahmed
1 Rollini, Simone Fulvio
1 Schachte, Peter
1 Schlaipfer, Matthias
1 Schröer, Philipp
1 Shakerin, Farhad
1 Shankar, Natarajan
1 Sharygina, Natasha
1 Shved, P. E.
1 Søndergaard, Harald
1 Stuckey, Peter James
1 Sun, Jiaguang
1 Tassing, Remi
1 Teige, Tino
1 Totla, Nishant
1 Tsitovich, Aliaksei
1 Voronkov, Andrei
1 Weissenbacher, Georg
1 Wernhard, Christoph
1 Wies, Thomas
1 Xia, Bican
...and 6 more Authors

Referencing Publications by Year