Publications
2024
 Salwa Tabet Gonzalez, Predrag Janicic, Julien Narboux: Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving. EPTCS 398, 2024, pp. 2137
2023
 Milan Bankovic, Ivan Drecun, Filip Maric. A proof system for graph (non)isomorphism verification. Logical Methods in Computer Science. 2023.
 Milan Banković. Automation of Triangle RulerandCompass Constructions Using Constraint Solver, presented at ADG 2023.
 Predrag Janicic, Julien Narboux: Automated generation of illustrated proofs in geometry and beyond. Ann. Math. Artif. Intell. 91(6): 797820 (2023)
2022
 Milan Banković, David Šćepanović.Trail Saving in SMT. Presented at SMT workshop 2022 (part of FLOC 2022).
 Predrag Janicic, Julien Narboux: Theorem Proving as Constraint Solving with Coherent Logic. J. Autom. Reason. 66(4): 689746 (2022)
2021
 Milan Banković, Filip Marić. Faradžev Readtype enumeration of nonisomorphic CC systems. Computational Geometry 97 (2021): 101770.
 Milan Banković. Automated solving of Sokoban puzzle using artificial intelligence. Presented at YU INFO 2021, Kopaonik, Serbia (in Serbian).
2020
 Mirko Spasić, Milena Vujošević Janičić: Verification supported refactoring of embedded SQL. Software Quality Journal (2020).
 Milena Vujošević Janičić: Concurrent Bug Finding Based on Bounded Model Checking. Int. J. Softw. Eng. Knowl. Eng. 30(5): 669694 (2020)
 Milica Selaković, Vesna Marinković, Predrag Janičić: New Dynamics in Dynamic Geometry: Dragging Constructed Points, Journal of Symbolic Computation, Volume 97, March–April 2020, Pages 315.
 Milena Vujošević Janičić, Filip Marić: Regression verification for automated evaluation of students programs. Comput. Sci. Inf. Syst. 17(1): 205227 (2020)
2019
 Predrag Janičić, Filip Marić, Marko Maliković: ComputerAssisted Proving of Combinatorial Conjectures Over Finite Domains: A Case Study of a Chess Conjecture Logical Methods in Computer Science, Volume 15, Issue 1, 2019, pp. 34:1–34:37
 Mladen Nikolić, Vesna Marinković, Zoltan Kovacs, Predrag Janičić: Portfolio Theorem Proving and Prover Runtime Prediction for Geometry, Annals of Mathematics and Artificial Intelligence, Issue 24/2019.
2018
 Sana Stojanovic Djurdjevic: From informal to formal proofs in Euclidean geometry, Annals of Mathematics and Artificial Intelligence, Issue 85, pp 89117 [pdf]
 Julien Narboux, Predrag Janičić, Jacques Fleuriot: ComputerAssisted Theorem Proving in Synthetic Geometry Handbook of Geometric Constraint Systems Principles (editors Meera Sitharam, Audrey St. John, Jessica Sidman), pp 2160, Chapman and Hall/CRC, Taylor & Francis Group, 2018.
 Milutin Pejović, Mladen Nikolić, Gerard Huevelink, Tomislav Hengl, Milan Kilibarda, Branislav Bajat:
Sparse Regression Interaction Models for Spatial Prediction of Soil Properties in 3D, Computers and Geosciences, 2018.
 Milutin Pejović, Mladen Nikolić, Branislav Bajat:
3D Soil Texture Mapping with L1 Regularized Multinomial Logistic Regression, 19th Annual Conference of International Association for Mathematical Geosciences (IAMG), 2018.
2017
 Dragan Lambić, Mladen Nikolić:
PseudoRandom Number Generator Based on DiscreteSpace Chaotic Map, Nonlinear Dynamics, 2017.
2016
 Predrag Janičić: Geometrisation of Geometry (invited talk), presented at ADG 2016.
[pdf]  Vesna Marinković, Mladen Nikolić, Zoltan Kovacs, Predrag
Janičić: Portfolio Methods in Theorem Proving for Elementary Geometry,
presented at ADG 2016.
[pdf]  Pascal Schreck, Pascal Mathis, Vesna Marinković, Predrag
Janičić: Wernick's List: A Final Update, Forum Geometricorum,
vol 16, pp. 6980, 2016.
[pdf] 
Pascal Schreck, Vesna Marinković, Predrag Janičić, Constructibility Classes for
Triangle Location Problems,
Mathematics in Computer Science, Springer,
vol 10, issue 1, pp. 2739, 2016.
[pdf]  Milan Banković: Parallelizing simplex within SMT solvers,
Artificial Intelligence Review, accepted for publication, 2016.
[pdfdraft], [DOI]  Milan Banković: Solving finitedomain linear constraints in presence of the alldifferent,
Logical Methods in Computer Science, Vol. 12, issue 3, 2016.
[pdfdraft], [LMCS]  Milan Banković: Improving SMT solvers using CSP techniques and parallelization techniques. PhD
Thesis (Serbian), December 2016.
[pdf]
2015
 Vesna Marinković: Online Compendium of Triangle Construction
Problems with Automatically Generated Solutions,
The Teaching of Mathematics, XVIII_1, pp. 2944, 2015.
[pdf] 
Filip Marić: A Survey of Interactive Theorem Proving, accepted for publication, 2015.
[pdf] 
Filip Marić, Predrag Janičić, Marko Maliković: Proving Correctness of a KRK Chess Endgame Strategy by using Isabelle/HOL and Z3, In 25th International Conference on Automated Deduction  CADE 25, Volume 9195 of the series Lecture Notes in Computer Science, pp 256271.
[pdf]  Vesna Marinković, Predrag Janičić, Pascal Schreck: Computer Theorem Proving for
Verifiable Solving of Geometric Construction Problems, In F. Botana and
P. Quaresma, editors, Automated Deduction in Geometry, ADG 2014,
volume 9201 of Lecture Notes in Computer Science, pp. 7293. Springer, 2015.
[pdf]  Vesna Marinković: ArgoTriCS  Automated Triangle Construction Solver,
Journal of Experimental & Theoretical Artificial Intelligence, accepted for publication
[pdfdraft]  Vesna Marinković: Automated Solving of Construction Problems in Geometry. PhD
Thesis (Serbian), June 2015.
[pdf]  Milan Banković: Extending SMT solvers with support for finite domain alldifferent constraint,
Constraints, accepted for publication, 2015
[pdfdraft], [DOI]
2014
 Sana Stojanovic Djurdjevic, Julien Narboux, Predrag Janicic: Automated Generation of Machine Verifiable and Readable Proofs: A Case Study of Tarski's Geometry, Annals of Mathematics and Artificial Intelligence, accepted for publication [pdf]
 Milena Vujošević Janičić: System LAV and Automated Evaluation of Students’ Programs,
Dagstuhl Reports, Volume 4, Issue 8, 2014.
[pdf]  Filip Marić, Danijela Petrović: Formalizing Complex Plane Geometry. Annals of Mathematics and Artificial Intelligence, Springer, accepted, 2014. [pdf]
 Mirko Stojadinović: Air Traffic Controller Shift Scheduling by Reduction to CSP, SAT and SATrelated Problems, CP 2014, 8656, 2014.
 Mirko Stojadinović, Filip Marić: meSAT: Multiple Encodings of CSP to SAT, Constraints, 19(4), 2014. [pdfdraft]
 Jelena Slivka, Mladen Nikolić, Kosta Ristovski, Vladan Radosavljević, Zoran Obradović: Distributed Gaussian Conditional Random Fields Based Regression for Large Evolving Graphs, SIAM International Conference on Data Mining, Workshop on Mining Networks and Graphs, 2014.
 Sana Stojanović, Julien Narboux, Marc Bezem, Predrag Janičić: A Vernacular for Coherent Logic, Intelligent Computer Mathematics  CICM 2014, Lecture Notes in Computer Science, Volume 8543, Springer [pdf]
 Vesna Marinković, Predrag Janičić, Pascal Schreck: Solving Geometric Construction Problems Supported by Theorem Proving,
presented at ADG 2014.
[pdf]  Vesna Marinković: Proof Simplification in the Framework of Coherent Logic, Computing and Informatics, vol 34, no. 02, pp. 337366, 2015.
[pdfdraft]
2013
 Mladen Nikolić: Guiding Search in Automathed Theorem Proving. PhD Thesis (Serbian), May 2013. [pdf]
 Marko Maliković, Predrag Janičić: Proving Correctness of a KRK Chess Endgame Strategy by SATbased Constraint Solving. ICGA Journal (International Computer Games Association), June 2013. [pdfdraft]
 Milena VujoševićJaničić, Mladen Nikolić, Dušan Tošić, Viktor Kuncak: Software Verification and Graph Similarity for Automated Evaluation of Students' Assignments. Information and Software Technology, Elsevier 2013. [ DOI ]
 Sana Stojanović: Preprocessing of the Axiomatic System for More Efficient Automated Proving and Shorter Proofs. Automated Deduction in Geometry, Lecture Notes in Computer Science, Volume 7993, Springer [pdf]
 Mladen Nikolić, Filip Marić, Predrag Janičić: Simple Algorithm Portfolio for SAT,
Artificial Intelligence
Review, Volume 40, Issue 4, 2013.
[pdf]
2012
 Predrag Janičić: Uniform Reduction to SAT. Logical Methods in Computer Science, Volume 8, Issue 3, Paper 30, 2012.
 Tomislav Hengl, Mladen Nikolić, Robert MacMillan: Mapping Efficiency and Information Content. International Journal of Applied Earth Observation and Geoinformation, 2012. [DOI]
 Mirko Spasić, Filip Marić: Formalization of Incremental Simplex Algorithm by Stepwise Refinement. In FM2012  18th International Symposium on Formal Methods, LNCS 7436, Springer, 2012. [pdf] [slides]
 Danijela Petrović, Filip Marić: Formalizing Analytic Geometries. Presented at ADG2012  Automated Deductinon in Geometry, Edinburgh, UK, 2012.

Mladen Nikolić, Predrag Janičić:
CDCLBased Abstract State Transition System for Coherent Logic.
In J. Jeuring et al. (Eds.): Intelligent Computer Mathematics, (CICM 2012),
LNAI 7362, pp. 263–278, 2012.
[pdf] 
Vesna Marinković, Predrag Janičić:
Towards Understanding Triangle Construction Problems.
In J. Jeuring et al. (Eds.): Intelligent Computer Mathematics, (CICM 2012),
LNAI 7362, pp. 126–141, 2012.
[pdf] 
Filip Marić, Miodrag Živković, Bojan Vučković: Formalizing Frankl's Conjecture: FCfamilies. In J. Jeuring et al. (Eds.):
Intelligent Computer Mathematics (CICM 2012). Calculemus track. LNAI 7362, 2012.
[pdf]  Filip Marić, Ivan Petrović, Danijela Petrović, Predrag Janičić: Formalization and Implementation of Algebraic Methods in Geometry. In Pedro Quaresma and RalphJohan Back: Proceedings First Workshop on CTP Components for Educational Software (THedu'11), Wrocław, Poland, 31th July 2011, Electronic Proceedings in Theoretical Computer Science 79, pp. 63–81.
 Milena VujoševićJaničić, Viktor Kuncak: Development and Evaluation of LAV: an SMTBased Error Finding Platform. Verified Software: Theories, Tools, Experiments. Lecture Notes in Computer Science, Volume 7152, Springer 2012, ISBN 9783642277047.
[pdf] [slides]  Milan Banković: ArgoSMTExpression: an SMTLIB 2.0 compliant expression library, presented at Pragmatics of SAT 2012.
[pdf] [slides]  Mladen Nikolić: Measuring Similarity of Graph Nodes by Neighbor Matching,
Intelligent Data Analysis,
Volume 40, Issue 4, 2012.
[pdf]
2011
 Sana Stojanović, Vesna Pavlović, Predrag Janičić: A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs. Automated Deduction in Geometry, Lecture Notes in Computer Science, Volume 6877, Springer. [pdf]
 Predrag Janičić: Automated Reasoning: Some Successes and New Challenge,
Proceedings of 22nd Central European Conference on Information and Intelligent Systems,
CECiiS 2011 (Invited lecture), 2011.
[pdf]  Predrag Janičić, Julien Narboux, Pedro Quaresma: The Area Method: A Recapitulation. Journal of Automated Reasoning, to appear. [pdf]
 Filip Marić, Predrag Janičić: Formalization of Abstract State Transition Systems for SAT, Logical Methods in Computer Science, 7(3), 2011.
[pdf]
2010
 Filip Marić: Formal Verification of a Modern SAT Solver by Shallow Embedding into Isabelle/HOL, Theoretical Computer Science, Volume 411, Number 50, 2010.
[pdf]  Predrag Janičić: Geometry Construction Language, Journal of Automated Reasoning, Volume 44, Issue 12, 2010.
[pdf]  Filip Marić, Predrag Janičić: Formal Correctness Proof for DPLL Procedure, Informatica, Volume 21, Number 1, 5778, 2010
[pdf]  Mladen Nikolić: Statistical Methodology for Comparison of SAT Solvers, In Theory and Applications of Satisfiability Testing  SAT 2010, LNCS 6175, pp. 209222, Springer, 2010.
[pdf] [slides]  Filip Marić, Predrag Janičić: URBiVA: Uniform Reduction to BitVector Arithmetic, presented at IJCAR 2010.
[pdf] [slides]  Sana Stojanović, Vesna Pavlović, Predrag Janičić: Automated Generation of Formal and Readable Proofs in Geometry Using Coherent Logic, presented at ADG
2010.
[pdf] [slides]  Milan Banković, Filip Marić: An Alldifferent Constraint Solver in SMT, presented at SMT Workshop 2010.
[pdf] [slides]
2009
 Mladen Nikolić, Filip Marić, Predrag Janičić: Instance Based Selection of Policies for SAT Solvers, In Theory and Applications of Satisfiability Testing, LNCS 5584, pp. 326340, Springer, 2009.
[pdf]  Filip Marić: Formalization
and Implementation of Modern SAT Solvers, Journal of Automated Reasoning 43(1), pp.~81119, Springer,
2009.
[pdf]  Filip Marić, Predrag Janičić: SAT Verification project, TPHOLs 2009, Emerging trends, pp. 4049.
[pdf]  Filip Marić: Formalization, Implementation and Verification of SAT solvers. PhD Thesis (Serbian), june 2009.
[pdf]
2008
 Mladen Nikolić. Methodolgy for choosing suitable values of parameters of
SAT solvers. Master Thesis (Serbian), December 2008.
[pdf]  Pedro Quaresma, Predrag Janičić, Jelena Tomašević, Milena Vujošević Janičić, Dušan Tošić. XMLbased Format for Geometry  XMLbased Format for Descriptions of Geometrical Constructions and Geometrical Proofs. Chapter in Communicating Mathematics in Digital Era, edited by. J. M. Borwein, E. M. Rocha and J. F. Rodrigues, Pages 183  197, 2008.
[pdf]  Jelena Tomašević. XML databases and their applications in lexical resources management. Master Thesis, September 2008.
[pdf]  Milena VujoševićJaničić. Ensuring Safe Usage of Buffers in Programming Language C. In Proceedings of ICSOFT 2008  Third International Conference on Software and Data Technologies, Volume PL/DPS/KE, Pages 29  36, 2008.
[pdf] [slides] 
Milena VujoševićJaničić.
Automated Detection of Buffer Overflows in Programming Language C. Master Thesis, June 2008.
[pdf]  Milena VujošvićJaničić, Filip Marić, Dušan Tošić. Using Simplex Method in Verifying Software Safety. In Proceedings of BALCOR 2007  Eight Balkan Conference on Operetional Research, Pages 305  319, 2008.
[pdf]
2007
 Predrag Janičić, Pedro Quaresma. Automated Verification of Regular Constructions. Automated Deduction in Geometry, Lecture Notes in Artificial Intelligence, SpringerVerlag, Volume 4869, 2007.

Predrag Janičić, Alan Bundy. Automatic synthesis of decision procedures. Calculemus, Springer, Lecture Notes in Artificial Intelligence, Volume 4573, Pages 80  93, 2007.
[shortpdf] [ longpdf] [code] [slides]  Pedro Quaresma, Predrag Janičić. GeoThms — a Web System for Euclidean Constructive Geometry, Proceedings of the 7th Workshop on User Interfaces for Theorem Provers (UITP 2006), Electronic Notes in Theoretical Computer Science, Volume 174, Issue 2, Pages 35  48, 15 May 2007.
 Andrija Tomović, Predrag Janičić. A Variant of Ngrambased Classification of Languages, AI*IA, Lecture Notes in Artificial Intelligence, Volume 4733, Pages 410  421, 2007.
 Milena VujoševićJaničić, Jelena Tomašević, Predrag Janičić. Random kGDSAT Model and its Phase Transition. Journal of Universal Computer Science, Volume 13, Issue 4, Pages 572  591, 2007.
2006

Predrag Janičić. GCLC  A Tool for Constructive Euclidean Geometry and More than That. International Congress of Mathematical Software (ICMS 2006), Takayama, Nobuki and Iglesias, Andres and Gutierrez, Jaime, editors. Lecture Notes in Computer Science, SpringerVerlag, Volume 4151, Pages 58  73, 2006.
[pdf] [slides] 
Predrag Janičić, Pedro Quaresma. System Description: GCLCprover + GeoThms. International Joint Conference on Automated Reasoning (IJCAR2006), Furbach, Ulrich and Shankar, Natarajan, editors. SpringerVerlag, Lecture Notes in Artificial Intelligence, Volume 4130, Pages 145  150, 2006.
[pdf]  Predrag Janičić, Pedro Quaresma. Automatic Verification of Regular Constructions in Dynamic Geometry Systems, Automated Deduction in Geometry, Pages 39  51, 2006.
 Petar Maksimović, Predrag Janičić. Simple characterization of functionally complete oneelement sets of propositional connectives. Mathematical Logic Quarterly, 52(5), Pages 498  504, 2006.

Miroslav Marić, Sana Stojanović. Adaptation of Edges in a Triangular Mesh. SISY 2006  4th SerbianHungarian Joint Symposium on Intelligent Systems, 2006.
[pdf] 
Pedro Quaresma, Predrag Janičić. Integrating Dynamic Geometry SoftwareDeduction Systems, and Theorem Repositories, Mathematical Knowledge Management (MKM2006), Borwein, J.M. and Farmer, W.M, editors. Lecture Notes in Artificial Intelligence, Volume 4108, SpringerVerlag, Pages 280  294, 2006.
[pdf] 
Andrija Tomović, Predrag Janičić, Vlado Kešelj. Ngrambased Classification and Unsupervised Hierarchical Clustering of Genome Sequences, Computer Methods and Programs in Biomedicine, Elsevier, Volume 8, Issue 2, Pages 137  153, 2006.
[pdf]
2005

Dejan Jovanović, Predrag Janičić. Logical Analysis of Hash Functions. Frontiers of Combining Systems (FroCoS), Springer, Lecture Notes in Artificial Intelligence, Volume 3717, Pages 200  215, 2005.
[pdf] [slides]
2004

Mirjana Đorić, Predrag Janičić. Constructions, Instructions, Interactions, Teaching Mathematics and its Applications. Oxford University Press, Volume 23, Issue 2, Pages 69  88, 2004.
[pdf]  Filip Marić, Borovčanin Momčilo, Miroslav Marić. Quantifier elimination in fields. ETRAN, 2004.
[pdf]  Filip Marić, Predrag Janičić. SMTLIB in XML clothes. Proceedings of the 2nd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2004), Dublin, July 2004.
[shortpdf] [longpdf]  Filip Marić, Predrag Janičić. ARGOLIB: A Generic Platform for Decision Procedures. IJCAR04, Springer, Lecture Notes in Artificial Intelligence, Volume 3097, Pages 213  217, 2004.
[pdf]