×

zbMATH — the first resource for mathematics

Kuncak, Viktor

Compute Distance To:
Author ID: kuncak.viktor Recent zbMATH articles by "Kuncak, Viktor"
Published as: Kuncak, Viktor; Kunčak, Viktor
External Links: MGP
Documents Indexed: 47 Publications since 2000, including 3 Books

Publications by Year

Citations contained in zbMATH

31 Publications have been cited 125 times in 75 Documents Cited by Year
Towards efficient satisfiability checking for Boolean algebra with Presburger arithmetic. Zbl 1213.03021
Kuncak, Viktor; Rinard, Martin
10
2007
Deciding Boolean algebra with Presburger arithmetic. Zbl 1112.03011
Kuncak, Viktor; Nguyen, Huu Hai; Rinard, Martin
9
2006
Combining theories with shared set operations. Zbl 1193.03030
Wies, Thomas; Piskac, Ruzica; Kuncak, Viktor
8
2009
Using first-order theorem provers in the Jahob data structure verification system. Zbl 1132.68348
Bouillaguet, Charles; Kuncak, Viktor; Wies, Thomas; Zee, Karen; Rinard, Martin
8
2007
An algorithm for deciding BAPA: Boolean algebra with Presburger arithmetic. Zbl 1102.03303
Kuncak, Viktor; Nguyen, Huu Hai; Rinard, Martin
8
2005
Sets with cardinality constraints in satisfiability modulo theories. Zbl 1317.68124
Suter, Philippe; Steiger, Robin; Kuncak, Viktor
7
2011
Counterexample-guided quantifier instantiation for synthesis in SMT. Zbl 1381.68059
Reynolds, Andrew; Deters, Morgan; Kuncak, Viktor; Tinelli, Cesare; Barrett, Clark
6
2015
Decision procedures for algebraic data types with abstractions. Zbl 1312.68147
Suter, Philippe; Dotta, Mirco; Kuncak, Viktor
6
2010
Decision procedures for multisets with cardinality constraints. Zbl 1138.68528
Piskac, Ruzica; Kuncak, Viktor
6
2008
Induction for SMT solvers. Zbl 1432.68418
Reynolds, Andrew; Kuncak, Viktor
5
2015
Towards complete reasoning about axiomatic specifications. Zbl 1317.68117
Jacobs, Swen; Kuncak, Viktor
5
2011
Generalized typestate checking for data structure consistency. Zbl 1111.68509
Lam, Patrick; Kuncak, Viktor; Rinard, Martin
5
2005
Generalized records and spatial conjunction in role logic. Zbl 1104.68021
Kuncak, Viktor; Rinard, Martin
5
2004
An efficient decision procedure for imperative tree data structures. Zbl 1341.68034
Wies, Thomas; Muñiz, Marco; Kuncak, Viktor
4
2011
Collections, cardinalities, and relations. Zbl 1273.03110
Yessenov, Kuat; Piskac, Ruzica; Kuncak, Viktor
4
2010
Field constraint analysis. Zbl 1176.68130
Wies, Thomas; Kuncak, Viktor; Lam, Patrick; Podelski, Andreas; Rinard, Martin
4
2006
Boolean algebra of shape analysis constraints. Zbl 1202.68250
Kuncak, Viktor; Rinard, Martin
4
2004
Contract-based resource verification for higher-order functions with memoization. Zbl 1380.68099
Madhavan, Ravichandhran; Kulal, Sumith; Kuncak, Viktor
3
2017
Accelerating interpolants. Zbl 1374.68291
Hojjat, Hossein; Iosif, Radu; Konečný, Filip; Kuncak, Viktor; Rümmer, Philipp
3
2012
On recursion-free Horn clauses and Craig interpolation. Zbl 1322.68134
Rümmer, Philipp; Hojjat, Hossein; Kuncak, Viktor
2
2015
Linear arithmetic with stars. Zbl 1155.68406
Piskac, Ruzica; Kuncak, Viktor
2
2008
Existential heap abstraction entailment is undecidable. Zbl 1067.68054
Kuncak, Viktor; Rinard, Martin
2
2003
Solving quantified linear arithmetic by counterexample-guided instantiation. Zbl 1377.68138
Reynolds, Andrew; King, Tim; Kuncak, Viktor
1
2017
Verifying and synthesizing software with recursive functions (invited contribution). Zbl 1409.68065
Kuncak, Viktor
1
2014
Synthesis for unbounded bit-vector arithmetic. Zbl 1358.68198
Spielmann, Andrej; Kuncak, Viktor
1
2012
Ordered sets in the calculus of data structures. Zbl 1287.03073
Kuncak, Viktor; Piskac, Ruzica; Suter, Philippe
1
2010
Building a calculus of data structures. Zbl 1273.68100
Kuncak, Viktor; Piskac, Ruzica; Suter, Philippe; Wies, Thomas
1
2010
Runtime checking for separation logic. Zbl 1138.68456
Nguyen, Huu Hai; Kuncak, Viktor; Chin, Wei-Ngan
1
2008
Polynomial constraints for sets with cardinality bounds. Zbl 1195.68049
Marnette, Bruno; Kuncak, Viktor; Rinard, Martin
1
2007
Role analysis. Zbl 1323.68378
Kuncak, Viktor; Lam, Patrick; Rinard, Martin
1
2002
Confluence of untyped lambda calculus via simple types. Zbl 1042.03016
Ghilezan, Silvia; Kuncak, Viktor
1
2001
Contract-based resource verification for higher-order functions with memoization. Zbl 1380.68099
Madhavan, Ravichandhran; Kulal, Sumith; Kuncak, Viktor
3
2017
Solving quantified linear arithmetic by counterexample-guided instantiation. Zbl 1377.68138
Reynolds, Andrew; King, Tim; Kuncak, Viktor
1
2017
Counterexample-guided quantifier instantiation for synthesis in SMT. Zbl 1381.68059
Reynolds, Andrew; Deters, Morgan; Kuncak, Viktor; Tinelli, Cesare; Barrett, Clark
6
2015
Induction for SMT solvers. Zbl 1432.68418
Reynolds, Andrew; Kuncak, Viktor
5
2015
On recursion-free Horn clauses and Craig interpolation. Zbl 1322.68134
Rümmer, Philipp; Hojjat, Hossein; Kuncak, Viktor
2
2015
Verifying and synthesizing software with recursive functions (invited contribution). Zbl 1409.68065
Kuncak, Viktor
1
2014
Accelerating interpolants. Zbl 1374.68291
Hojjat, Hossein; Iosif, Radu; Konečný, Filip; Kuncak, Viktor; Rümmer, Philipp
3
2012
Synthesis for unbounded bit-vector arithmetic. Zbl 1358.68198
Spielmann, Andrej; Kuncak, Viktor
1
2012
Sets with cardinality constraints in satisfiability modulo theories. Zbl 1317.68124
Suter, Philippe; Steiger, Robin; Kuncak, Viktor
7
2011
Towards complete reasoning about axiomatic specifications. Zbl 1317.68117
Jacobs, Swen; Kuncak, Viktor
5
2011
An efficient decision procedure for imperative tree data structures. Zbl 1341.68034
Wies, Thomas; Muñiz, Marco; Kuncak, Viktor
4
2011
Decision procedures for algebraic data types with abstractions. Zbl 1312.68147
Suter, Philippe; Dotta, Mirco; Kuncak, Viktor
6
2010
Collections, cardinalities, and relations. Zbl 1273.03110
Yessenov, Kuat; Piskac, Ruzica; Kuncak, Viktor
4
2010
Ordered sets in the calculus of data structures. Zbl 1287.03073
Kuncak, Viktor; Piskac, Ruzica; Suter, Philippe
1
2010
Building a calculus of data structures. Zbl 1273.68100
Kuncak, Viktor; Piskac, Ruzica; Suter, Philippe; Wies, Thomas
1
2010
Combining theories with shared set operations. Zbl 1193.03030
Wies, Thomas; Piskac, Ruzica; Kuncak, Viktor
8
2009
Decision procedures for multisets with cardinality constraints. Zbl 1138.68528
Piskac, Ruzica; Kuncak, Viktor
6
2008
Linear arithmetic with stars. Zbl 1155.68406
Piskac, Ruzica; Kuncak, Viktor
2
2008
Runtime checking for separation logic. Zbl 1138.68456
Nguyen, Huu Hai; Kuncak, Viktor; Chin, Wei-Ngan
1
2008
Towards efficient satisfiability checking for Boolean algebra with Presburger arithmetic. Zbl 1213.03021
Kuncak, Viktor; Rinard, Martin
10
2007
Using first-order theorem provers in the Jahob data structure verification system. Zbl 1132.68348
Bouillaguet, Charles; Kuncak, Viktor; Wies, Thomas; Zee, Karen; Rinard, Martin
8
2007
Polynomial constraints for sets with cardinality bounds. Zbl 1195.68049
Marnette, Bruno; Kuncak, Viktor; Rinard, Martin
1
2007
Deciding Boolean algebra with Presburger arithmetic. Zbl 1112.03011
Kuncak, Viktor; Nguyen, Huu Hai; Rinard, Martin
9
2006
Field constraint analysis. Zbl 1176.68130
Wies, Thomas; Kuncak, Viktor; Lam, Patrick; Podelski, Andreas; Rinard, Martin
4
2006
An algorithm for deciding BAPA: Boolean algebra with Presburger arithmetic. Zbl 1102.03303
Kuncak, Viktor; Nguyen, Huu Hai; Rinard, Martin
8
2005
Generalized typestate checking for data structure consistency. Zbl 1111.68509
Lam, Patrick; Kuncak, Viktor; Rinard, Martin
5
2005
Generalized records and spatial conjunction in role logic. Zbl 1104.68021
Kuncak, Viktor; Rinard, Martin
5
2004
Boolean algebra of shape analysis constraints. Zbl 1202.68250
Kuncak, Viktor; Rinard, Martin
4
2004
Existential heap abstraction entailment is undecidable. Zbl 1067.68054
Kuncak, Viktor; Rinard, Martin
2
2003
Role analysis. Zbl 1323.68378
Kuncak, Viktor; Lam, Patrick; Rinard, Martin
1
2002
Confluence of untyped lambda calculus via simple types. Zbl 1042.03016
Ghilezan, Silvia; Kuncak, Viktor
1
2001
all top 5

Cited by 160 Authors

8 Kuncak, Viktor
6 Reynolds, Andrew
5 Wies, Thomas
4 Barrett, Clark W.
4 Fontaine, Pascal
4 Ringeissen, Christophe
4 Tinelli, Cesare
3 Blanchette, Jasmin Christian
3 Holík, Lukáš
3 Lengál, Ondřej
3 Vojnar, Tomáš
2 Alberti, Francesco
2 Banerjee, Anindya
2 Bansal, Kshitij
2 Biere, Armin
2 Böhme, Sascha
2 Bonacina, Maria Paola
2 Chin, Wei-Ngan
2 Chocron, Paula Daniela
2 Demri, Stéphane P.
2 Deters, Morgan
2 Dross, Claire
2 Echenim, Mnacho
2 Fiedor, Tomáš
2 Ghilardi, Silvio
2 Iosif, Radu
2 Lynch, Christopher A.
2 Nguyen, Huu Hai
2 Pagani, Elena
2 Paulson, Lawrence Charles
2 Piskac, Ruzica
2 Qin, Shengchao
2 Smallbone, Nicholas
2 Suter, Philippe
1 Abdulla, Parosh Aziz
1 Aliev, Iskander M.
1 Alur, Rajeev
1 Areces, Carlos
1 Balaban, Ittai
1 Bednarczyk, Bartosz
1 Bjørner, Nikolaj S.
1 Borba, Paulo
1 Boström, Pontus
1 Bouajjani, Ahmed
1 Bozga, Marius
1 Brinkop, Hauke
1 Brochenin, Rémi
1 Charguéraud, Arthur
1 Charlton, Nathaniel
1 Christ, Jürgen
1 Claessen, Koen
1 Conchon, Sylvain
1 Damm, Werner
1 David, Cristina
1 De Loera, Jesús A.
1 de Moura, Leonardo
1 Eisenbrand, Friedrich
1 Filliâtre, Jean-Christophe
1 Francis, Michael H.
1 Fröhlich, Andreas M.
1 Gacek, Andrew
1 Gheyi, Rohit
1 Gurfinkel, Arie
1 He, Guanhua
1 Hoenicke, Jochen
1 Hoffmann, Jan-Philipp
1 Horbach, Matthias
1 Inala, Jeevana Priya
1 Jacobs, Swen
1 Janků, Petr
1 Jansen, Christina
1 Jha, Susmit
1 Johansson, Moa
1 Jonsson, Bengt
1 Kamareddine, Fairouz D.
1 Kanig, Johannes
1 Katelaan, Jens
1 King, Tim
1 Köksal, Ali Sinan
1 Kontchakov, Roman
1 Kovásznai, Gergely
1 Kramer, Simon
1 Kröning, Daniel
1 Lasaruk, Aless
1 Lerner, Benjamin S.
1 Leroux, Jérôme
1 Lewis, Matthew S.
1 Lichtman, Benjamin
1 Lozes, Etienne
1 Malecha, Gregory
1 Malkis, Alexander
1 Manna, Zohar
1 Massoni, Tiago
1 Matheja, Christoph
1 McMillan, Kenneth L.
1 Meng, Jia
1 Meyer, Antoine
1 Morrisett, Greg
1 Moy, Yannick
1 Muñiz, Marco
...and 60 more Authors

Citations by Year