After completing high school from Nepal, Bishoksan went to Central University of Las Villas, Cuba under the Nepalese government scholarship for his undergraduate education in computer science. Then, he received his masters degree in computational logic from Dresden University of Technology, Germany; Free University of Bozen-Bolzano, Italy; and New University of Lisbon, Portugal, all under the Erasmus Mundus programme, after which, he went ahead to complete his PhD from Roskilde University, Denmark specialising in automated Horn clauses verification.
Prior to joining IMDEA, Bishoksan was a research fellow at the school of computing and information systems at the University of Melbourne, Australia, where he continues as an honorary researcher. During the second quarter of 2015, he was a visiting researcher at NASA Ames Research Center in California working on resource analysis of avionics systems. Since October 2018, he has been serving as an assessor for the Australian Research Council.
Homepage: https://bishoksan.github.io/
Please tell us briefly about your current research. What do you find most exciting about it?
These days, we are more than ever dependent on software systems to carry our everyday activities and the trust in them is immense. However, despite being developed following a rigorous software development process, there is absolutely no guarantee of whether or not they possess the desired properties. Such an assurance is especially crucial in safety-critical systems (e.g., avionics systems, space missions, medical devices, etc.) as well as others (processors, servers, etc.) to avoid catastrophic loss of human lives or other resources. One way of formally ensuring such a guarantee is through the use of formal logic. Logic in computer science (LICS) or computational logic is a subfield of computer science which covers the intersection of (formal) logic and computer science, applying logic to solve computing problems and utilizing computing technology to aid logicians.
Automated program analysis (inferring/deciding properties of programs) is a hot topic in the LICS community. The common analysis problems include program verification (verify whether a program has a certain property or not), resource analysis (infer the amount of resources such as time, energy, memory etc. consumed by a program), (non)-termination analysis (decide whether a program terminates or not), precondition analysis (derive initial conditions of the program that respect some properties of interest) etc. These problems are undecidable, that is, no algorithm can decide whether any arbitrary program has a given property or not.
My current research focuses on automated program analysis problems such as the ones mentioned above using Constrained Horn clauses (CHC), a fragment of first-order logic, as the semantic representation of programs. In particular, I am interested in the logical encoding of these problems into CHC and their subsequent analysis. Depending on the program’s data structure, program structure and abstraction, and the property of interest and the encoding, CHC of varying complexity arise, wherein, my analysis approach involves abstract interpretation, program specialization, automata-theoretic approaches etc. Such analysis is useful, for example, in showing that a program is bug-free (free of undesired behaviours), terminating (never stuck in a loop), consuming a finite amount of resources and exhibiting some behaviour on a given set of input. Field-wise, my research interests fall under the categories of theoretical computer science, LICS, static analysis, (software) model checking and programming languages.
The most thrilling for me is to work on these undecidable problems. Though the general problem is undecidable, we should not be completely hopeless. This is because some (useful) fragments of it can still be decidable or a partial solution to the general problem can still be useful in practice. I enjoy these challenges.
How did you get interested in Computer Science and ‘Logic in Computer Science’ in particular? Tell us a bit about your career journey starting from your early school days.
I was born in a remote village of Tanahun and I completed my schooling from a local government school. Growing up in such a tiny village with many scarcities, I had not even imagined owning a computer and making a career in computer science.
After the completion of high school, many of my friends were moving to bigger cities and overseas for higher education but my financial situation did not allow me to think likewise. Fortunately, I got a scholarship for civil engineering in Cuba. So, I headed to Cuba for an engineering degree. However, it did not take long for me to realize that civil engineering was not something I was interested in. My interest was inclined towards computer science, as it was something new for me and my teachers were supportive of it given the fact that I was good and interested in mathematics. I was in a dilemma and had huge self-doubt on whether I would make a total mess of the opportunity which had been bestowed upon me but I carried on.
As destiny would have it, I completed bachelor’s in computer science with summa cum laude and returned back to Nepal, thinking of doing something in my own country. However, after a few months, I was disappointed over the situation of the country and the lack of employment opportunities. Once again the thought of moving abroad came to my mind and I applied for scholarships. I got an opportunity to do my master’s degree through the Erasmus Mundus Scholarship funding. This time my mindset had changed- there was no dilemma. Rather, I was enjoying what I was studying. I was confident and could see myself making my livelihood out of it. I completed my masters and moved on to do my doctoral and postdoctoral. Suddenly, these qualifications and my interest in the subject led me to a wealth of career transition opportunities. I got to work in prestigious institutions, research organizations and with reputed academics. Eventually, as of now, I am pursuing a satisfying career at IMDEA software institute and everything has been history since.
Please tell us more about ‘Logic in Computer Science’. It appears very influenced by theoretical subjects such as mathematics and philosophy. What are the practical applications of this field? How can this field be relevant to a developing country such as Nepal?
As mentioned earlier, logic in computer science (or computational logic) covers the intersection of logic and computer science. It applies logic to solve computational problems and uses computational techniques and resources to aid logicians. Logic is considered as the basis of all automated reasoning. The rules of logic specify the meaning of statements (either mathematical, philosophical or others) and help us understand and reason about them. For example, one can infer Ram is mortal from Ram is human and every human is mortal. In fact, this inference is valid. Therefore, in short, the rules of logic give a precise meaning to statements and can be used to distinguish between valid and invalid arguments.
Formal logic has been applied in mathematics, philosophy and computer science among others and there are well-established fields such as mathematical logic, philosophical logic and computational logic. The basis of all these is the following: any statement (philosophical, mathematical etc.) is formalised in a suitable logic and inference rules provided by that logic are used to reason about such statements. The logical conclusion (inference) is always a valid conclusion.
The field of computational logic is more closely tied to mathematical logic than to philosophical logic as computer science is closely tied to mathematics.
Computational logic is not only important in understanding computational reasoning, but it also has numerous applications in computer science, varying from the design of digital circuits, to the construction of computer programs and verification of correctness of programs. Many real-life problems can be encoded into some logic and reasoned formally about them. For example, software and hardware verification problems, consistency problems, etc. Since these are generic techniques, their application is not limited to any specific circumstances but whenever one needs to analyze and reason formally about the system under consideration. Specific examples in the context of Nepal may include checking the consistency/ambiguity of Nepalese constitution, verifying the correctness of many (in-house built) software/hardware systems such as drones, traffic lights, medical devices, communication devices, systems used for manipulating sensitive information etc.
What are the big problems in Computer Science/‘Logic in Computer Science’ that you are interested in?
I am interested in automated program analysis and verification in general which are undecidable problems (not only difficult but also have no complete algorithmic solutions). In particular, I am keen on the logical encoding of these problems into some appropriate logic and their subsequent analysis.
Tell us about a time you made an exciting breakthrough — or any other highlight in your journey so far.
There was a time during my PhD when I discovered a theoretical solution for solving nonlinear Horn clauses (set of clauses corresponding to a program with procedures) using a solver for linear Horn clauses in an iterative manner. I was very excited about its simplicity that easily yielded to practical implementations using a novel methodology for program analysis (Newton method from mathematics). This idea later got materialised and published here.
Tell us about a time you had serious doubts about your own ability in the fields you chose. How did you overcome that?
I cannot remember anything more vividly than an incident which occurred when I was in the second semester of my undergraduate education. As I have briefly mentioned above, after leaving the track of engineering and moving into computer science, I could not excel in programming which was one of the major parts of computer science. During that phase of the struggle, I encountered a lecturer who said that students should change their computing career if they did not have any interest in programming. I felt as if it was directed towards me. This statement implanted a sense of fear in me since I had already changed my course once and now I was not feeling confident enough to continue with the field I had moved into.
The whole situation filled me with self-doubt and for a moment I was afraid that I would lose my scholarship and would not make it in this field. To be honest, getting a scholarship was not only important because I wanted a good education but also because I could not afford it otherwise. This fact had a profound impact on my state of mind. Fortunately, I managed to work on those issues and I eventually regained my peace of mind, rekindling at the same time my sense of curiosity for the subject. I accepted the “challenge” and motivated myself to enjoy computer programming. This incident taught me one of the most valuable lessons during the pursuit of my career, that is, if you enjoy what you do the results will eventually follow.
If you were in the admissions committee, what qualities would you look into a prospective graduate candidate in your field?
First and foremost, the candidate must have an excellent academic record especially in subjects such as logic, (discrete) mathematics and programming languages. Other primary aspects to consider include the organization from where the degree is obtained, exposure beyond academia, publications and the letters of recommendation. In addition, the candidate must also be genuinely interested in the field and should have the ability to work in groups or independently, should be adaptable and open to learning new things. Above all, it is important that he/she is a good human being.
How can prospective graduate students prepare themselves for being a part of cutting edge research labs in your field?
To begin with, prospective students should have the right academic background (degree in computer science or computer engineering or informatics or mathematics or other closely related areas). It is also important that they are interested in the field and ready to work hard to achieve a career in it. As a next step, they can study formal logics (propositional, first-order logic, etc.) and declarative languages such as Prolog/Haskel in depth. They should also explore the connection between problems in computer science and logic. Last but not least, they should work on improving their academic writing and oral presentation skills and the English language in general.
Can you recommend 3 resources for people looking to get into your field ?
There are plenty of resources on the web nowadays. To find them one can use keywords such as program analysis, logic in computer science, formal methods, formal verification, abstract interpretation, satisfiability testing, SMT solving, etc. The following are few such examples.
Education material:
Formal methods in education: https://avigad.github.io/formal_methods_in_education/
Introduction to static program analysis (lecture notes): https://cs.au.dk/~amoeller/spa/
Abstract interpretation in a nutshell: www.di.ens.fr/~cousot/AI/IntroAbsInt.html
Social media groups:
Abstract interpretation: www.facebook.com/groups/abstract.interpretation/?epa=SEARCH_BOX
SMT solvers: https://twitter.com/SMT_Solvers
Mailing list and portals:
Formal methods and programming languages : https://lists.noisebridge.net/mailman/listinfo/formal-methods
Jobs and scholarships: https://www.researchprofessional.com
Competition problems:
Software verification competition: https://sv-comp.sosy-lab.org/2020/
Satisfiability solving competition: https://smt-comp.github.io/2019/index.html
You received your education and academic training from various countries. What are your observations and reflections?
Having gained my education both from Nepal and abroad, I see a huge polarity in the education system of Nepal and the western world in general. I would like to highlight the differences in terms of teaching and learning, research and engagement (commitment to ‘public values’).
Teaching and learning: Nepal’s education system, as opposed to the western one, still follows the traditional teaching approaches that put more focus on theoretical aspects and less on the application of the same. It rewards memorization as opposed to critical thinking and logical analysis. Teaching basically provides information; not knowledge and is not interactive at all. Students are directed to read textbooks rather than being engaged in practical projects to solve problems in science and technology. The academic grades are given more importance than the actual knowledge. But, the western education system has different assessment techniques and strategies compared to Nepal where creativity and critical thinking is highly prioritized.
Research: Research is almost non-existent in Nepal to the best of my knowledge. As a consequence, the country lacks innovation which is key to the development of the nation. This trend has been changing slowly with the emergence of research centres such as National Innovation Center, KIAS, NAAMI etc., but much is left to be done. We should follow the western model where substantial investment has been made in research and innovation.
Engagement: Our educational institutions are poorly engaged to stakeholders and to the general public, undermining its paramount importance to the benefit of our community and the country as a whole. As a consequence, the students and academics are unable to provide professional contributions and leadership and share advances that shape the country. In the west, however, engagement is pursued as complementary to research and teaching.
In summary, as opposed to Nepal’s education system, the western education system tries to balance the interplay between these key elements (Teaching, Research and Engagement).
What are your observations about the research scenario in Nepal? How can we make our education system more conducive to innovation and research?
I do not think it would be fair for me to make exact comments about the Nepalese research scenario without closely experiencing it. But in short, based on what is reflected on the outside and whatever little I know, compared to global setting, research scenario in Nepal is crippled and staggering far behind due to political interference, poor policies, nepotism, unemployment, poor national funding and educational system that is more focused on theoretical learning than practical experience which can neither engage its youth into resourceful manpower nor fulfill the practical needs of the society and the country as a whole.
My suggestion on making our education system more conducive to innovation and research primarily involves resolving my dissatisfaction expressed above. Nepal has got great talents, many youths are coming up with innovative ideas, so I guess the right platform and sustainable national projects should come into action first so that our youths do not feel discouraged.
Tell us about the role of mentorship in your professional life.
I would have never been where I am today, had I not had the support of mentors and supervisors who provided me consistent support throughout the journey. Mentorship assisted me not just professionally but also helped me to manage my personal life. During the juggle of university, assignment, lecture and research, the support of my mentors helped me immensely to maintain my integrity and they were constantly there to guide, motivate, and emotionally support me. The support is still ongoing.
I have so far had a sound career, all thanks to their assistance in helping me explore it, set goals, develop contacts, and identify resources. As it is said, home is your first school and the family is your first teacher; the moral and spiritual lessons underpinned in my childhood from my parents and siblings have always been the strong foundation and a point of support to look back onto.
What is the best career advice you have ever received?
You are capable of achieving anything that you truly believe in.
The career advice you wished you received in your twenties.
The choice of your career should be determined solely by your interests and dreams, not by your circumstances. This is the hard lesson I learnt from my bachelor’s degree.
Please share your experiences on opportunities and responsibilities of being at the forefront of cutting edge research as a Nepali national.
I feel really privileged to have received all my higher education from prestigious universities around the globe. This has not only exposed me to different educational systems, cultures, languages, people, etc. but has guaranteed placement into prestigious working environments where I’ve managed to evolve into the professional I am today. I have had opportunities to work with fellow researchers and students in some of the fundamental problems in computer science (discussed above) having both theoretical and practical values and contributed some solutions to a few problems in the field.
Being one of the very few Nepali nationals working in this field, I have to work hard in order not to jeopardize my countrymates’ dreams to attain the same level of success in the future. The challenges are still in front of me to transfer this knowledge and positive cultural experiences that I have learnt all along my way back to our country.
Your final words of advice for someone who wants to get into your field.
Have the courage to dive into the undecidable problems.
Leave a Reply