Bishoksan Kafle Research assistant, PhD student Roskilde University IMT, Building 08.2-053 Universitetsvej 1 DK-4000 Roskilde, Denmark Phone: +45 4674 3024 Fax: +45 4674 3075 E-mail: last name At ruc.dk ORCID iD: 0000-0001-5191-1216 Curriculum Vitae

PLIS Research Group

News

I am a research fellow at the department of Computing and Information Systems, the University of Melbourne (since June 2016). Please contact me @: bishoksank AT unimelb.edu.au.

Research

• Member of the Programming, Logic and Intelligent Systems research group in the Department of Communication, Business and Information Technologies at Roskilde University.
• Research Interests: Program analysis and verification.
• PhD: "Components for automatic Horn clause verification" under the supervision of Prof. John Gallagher.

Projects

• ENTRA: Whole-Systems Energy Transparency. European Commission Framework 7 project in the FET Proactive (MINECC) initiative. Partners University of Bristol, XMOS Ltd, and IMDEA Software Institute (2012-2015).

Publications (DBLP, Google Scholar)

• Bishoksan Kafle & John P. Gallagher & Pierre Ganty: Solving non-linear Horn clauses using a linear Horn clause solver, HCVS 2016 [PDF] .
• Bishoksan Kafle & John P. Gallagher : Interpolant automata and their application in Horn clause verification, VPT 2016 [PDF] .
• Bishoksan Kafle & John P. Gallagher : Horn clause verification with convex polyhedral abstraction and tree automata-based refinement, Journal of Computer Languages, Systems & Structures (COMLAN) 2015 [PDF] .
• Bishoksan Kafle & John P. Gallagher & Pierre Ganty: Decomposition by tree dimension in Horn clause verification, VPT 2015 [PDF] .
• Bishoksan Kafle & John P. Gallagher : Constraint Specialisation in Horn Clause Verification, PEPM 2015 (Best Paper Award) [PDF] [Slides] [BibTex].
• Bishoksan Kafle & John P. Gallagher : Tree automata-based refinement with application to Horn clause verification, VMCAI 2015 [PDF] [Slides] [BibTex].
• Bishoksan Kafle & John P.Gallagher: Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification, HCVS 2014 [PDF] [Slides] [BibTex].
• John P. Gallagher & Bishoksan Kafle: Analysis and Transformation Tools for Constrained Horn Clause Verification, ICLP (technical communication) 2014 [PDF] [Slides] [BibTex].

Talks

• Solving non-linear Horn clauses using a linear Horn clause solver: HCVS (03-04-2016), Eindhoven, Netherlands [Slides].
• Interpolant automata and their application in Horn clause verification: VPT (02-04-2016), Eindhoven, Netherlands [Slides].
• Solving non-linear Horn clauses using a linear solver: Roskilde University (04-11-2015), Denmark [Slides].
• Resource analysis of C programs by analysing its Horn clause representation: 2nd ICT-ENERGY international doctoral symposium (16-09-2015) Bristol, UK [Slides].
• Resource analysis of C programs by analysing its Horn clause representation: DANSAS (20-08-2015), Odense, Denmark [Slides].
• Static resource analysis with application to avionics systems: NASA Ames research center (29-05-2015), CA, US [Slides].
• Constraint Specialisation in Horn Clause Verification, PEPM 2015, Mumbai, India [Slides].
• Tree automata-based refinement with application to Horn clause verification, VMCAI 2015, Mumbai, India [Slides].
• Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification, HCVS 2014, Vienna [Slides].
• Analysis and Transformation Tools for Constrained Horn Clause Verification, ICLP 2014, Vienna [Slides].
• Program's resource verification as CHC solving: ENTRA plenary meeting (13/14-01-2014) Bristol, UK [Slides].
• Constrained Horn Clause Verification: ENTRA-SENSATION Workshop (13-05-2014) Aalborg, Denmark [Slides].

Teaching

• Scientific Computing (Autumn 2014)