Bishoksan Kafle, PhD APS@Australian Government, H. Research fellow@The university of Melbourne Phone: +61 416653634 E-mail: bishoksan At gmail.com ORCID iD: 0000-0001-5191-1216 Resume

Research Interests

Automated Reasoning, Program Analysis, Software Model Checking, Constraints Solving, Program Specialisation, Horn Clauses Analysis and Verification; Data Analytics, Generative AI, Cyber and Infracture Security.

Selected Softwares

• Tagr-Solver: Complexity Analyser Based On Regular Transformation Of Horn Clauses
• NtHorn: Non-Termination Precondition Inferer For Horn Clauses
• RAHFT: Solver For Horn Clauses
• PI-Horn: Safety Precondition Inferer For Horn Clauses
• LHornSolver: Horn Clause Solver With Incremental Linearisation

Selected Publications (DBLP, Google Scholar)

• Bishoksan Kafle, Graeme Gange, Peter J. Stuckey, Peter Schachte & Harald Sondergaard: A Lightweight Approach to Nontermination Inference Using Constrained Horn Clauses. SoSym. 2024. (to appear)
• Robert Glück & Bishoksan Kafle: Logic-Based Program Synthesis and Transformation - 33rd International Symposium, LOPSTR. LNCS 14330, Springer 2023, ISBN 978-3-031-45783-8.
• Hossein Hojjat & Bishoksan Kafle: Proceedings 8th Workshop on Horn Clauses for Verification and Synthesis. 2021. EPTCS vol. 344. ISSN: 2075-2180.
• Bishoksan Kafle, Graeme Gange, Peter J. Stuckey, Peter Schachte & Harald Sondergaard: Transformation-enabled precondition inference. TPLP. 2021.
• Bishoksan Kafle, Graeme Gange, Peter Schachte, Harald Sondergaard & Peter J. Stuckey: Lightweight Nontermination Inference with CHCs. SEFM. 2021.
• Bishoksan Kafle, John P. Gallagher, Manuel V. Hermenegildo et al.: Regular Path Clauses and Their Application in Solving Loops. HCVS. 2021.
• Bishoksan Kafle & John P. Gallagher & Graeme Gange & Peter Schachte & Harald Sondergaard & Peter J. Stuckey: An iterative approach to precondition inference using constrained Horn clauses, TPLP 2018 [PDF].
• Bishoksan Kafle & John P. Gallagher & Pierre Ganty: Tree dimension in verification of constrained Horn clauses, TPLP 2018 [PDF].
• Bishoksan Kafle & John P. Gallagher: Constraint Specialisation in Horn Clause Verification, SCP 2017 [PDF].
• Bishoksan Kafle & Graeme Gange & Peter Schachte & Harald Sondergaard & Peter J. Stuckey: A Benders Decomposition Approach to Deciding Modular Linear Integer Arithmetic, SAT 2017 [PDF].
• Bishoksan Kafle & John P. Gallagher: Horn clause verification with convex polyhedral abstraction and tree automata-based refinement, COMLAN 2017 [PDF].
• Bishoksan Kafle & John P. Gallagher & Jose F. Morales: Rahft: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata, CAV 2016 [PDF].
• Bishoksan Kafle & John P. Gallagher: Constraint Specialisation in Horn Clause Verification, PEPM 2015 (Best Paper Award) [PDF].
• John P. Gallagher & Bishoksan Kafle: Analysis and Transformation Tools for Constrained Horn Clause Verification, ICLP (technical communication) 2014 [PDF].

Services

• Accessor: Australian Research Council
• Reviewer: SCP, Journal of automated reasoning, TPLP, Fundamenta Informaticae, Formal Methods in System Design
• PC member: LOPSTR'17, VPT'18, HCVS'19, VPT'20, VMCAI-AE'20, LOPSTR'21, HCVS'21 (co-chair), iFM'22, LOPSTR'23 (co-chair), FormaliSE-AE'23, LOPSTR'24, HCVS'24
• Steering committee member: LOPSTR (2024-2029)

Interesting readings

• Vipassana Meditation by S.N. Goenka
• Buddhism plain and simple by Steve Hagen
• Mind Power Into the 21st Century by John Kehoe
• Man's Search for Meaning by Viktor E. Frankl
• The power of now by Eckhart Tolle