Nominations for four CADE trustee positions were being sought, in preparation for the elections to be held after IJCAR 2022.
The following candidates were nominated and their statements, in alphabetical order, are below:
My research covers various theoretical and practical aspects of automated deduction, mostly focused around SMT. CADE is my home conference. I attend CADE and IJCAR whenever possible. I believe that our (CADE) community is welcoming fundamental and theoretical works (that can sometimes be overlooked elsewhere because of lack of immediate applications), as well as more experimental and practical works (that can sometimes be overlooked elsewhere because of a lack of appreciation of the enormous amount of energy to develop software and practical experiments). Besides being open to a large range of research, I also believe our community is a friendly one, it is open to new ideas and is welcoming of new people, notably young PhD students. All these nice aspects must be preserved and improved, and this requires constant attention from all, particularly from PC chairs, PC members, and the Board of Trustees. I am thus honored to be nominated for the Board of Trustees. Elected or not, I will continue to work at my place for these important aspects in our research.
The Board of Trustees is crucial in maintaining an open and friendly environment for all, especially for young researchers. In particular, it is ensuring the continuity of the Woody Bledsoe Awards, the SAT/SMT/AR summer school and best student papers. Recently, the Bill McCune PhD Award was established. Besides sustaining these tools, I believe an important future work which is essential for openness is to think about hybrid conferencing. There is nothing equivalent to in-person attendance, but in-person is not always possible. There are financial aspects, people might not be able to attend in-person for health or family reasons, some are impacted by travel restrictions or difficulties to get VISAs, master students would not come for a week without funding, and an increasing number of people also have ethical concerns with traveling. The possibility to attend a talk remotely is probably something we could offer systematically for CADE to the world, for a reasonable price, without impacting at all the experience of the people attending in person. So why not do it? I believe this would contribute to openness towards many who for some reason cannot attend in person. This would give to master students a window to state-of-the-art research in automated deduction, and it might contribute to attract excellent PhD candidates. Were CADE remote attendance free, I would definitely advertise the conference to all students in my Logic course, and if remote attendance cost was not free but reasonable, I would fund attendance for a few selected master students each year. As a concrete example of a contribution as an elected member of the Board of Trustee, I would like to bring this discussion to the Board, so that this point is thoroughly discussed.
I still believe that the current cycle of conferences, CADE alternating with IJCAR, and IJCAR as a part of FLoC every four years, is the right organization for the current situation, since it preserves the specificity of CADE and of the other compound conferences of IJCAR. This must be done with coordination between CADE and the friend conferences like FroCoS, ITP, and Tableaux, e.g. to adjust dates and locations, and maybe sometimes experiment colocation.
My goal as a trustee would be to ensure that CADE keeps on being the main conference for all research in the area of automated deduction. Therefore, the scope of CADE should remain as broad as possible. CADE should be open to any aspect of automated deduction and it should cover everything from theoretical results and practical contributions up to applications of automated reasoning.
I also think that it is very important to attract tool submissions, and to organize tool competitions co-located with CADE. (Since its foundation in 2004, I have been active in the termination competition, which took place during IJCAR/CADE several times.)
I am also in favor of continuing the publication of CADE as an "open access" publication within LNCS, similar to the proceedings of CADE 2021 and IJCAR 2022.
I think the current organization of CADE as a stand-alone event every second year, within IJCAR every other year, and within FLoC every four years is still a very good solution to guarantee the visibility of CADE on its own, while keeping in close contact with neighboring meetings and fields.
To attract as many participants as possible and to allow students to attend the conference, I think CADE should aim at affordable conference fees and continue the very good tradition of Woody Bledsoe travel grants for students. While I am in favor of having physical meetings again, online participation should be possible as well to allow attendance also for researchers who cannot travel, e.g., due to financial or health constraints.
My own research is concerned with different aspects of automated deduction. Therefore, I have been attending and publishing papers at CADE since 1994. In particular, I am working on techniques and tools to analyze properties like termination or complexity of programs automatically.
I was one of the PC chairs of IJCAR 2010, PC chair of RTA 2005, Steering Committee chair of RTA (2005-2007), Area Editor of ACM TOCL (since 2013), SC member of FSCD (since 2022), and I served many times on the PCs of CADE, IJCAR, RTA, LPAR, FSCD, and several other conferences in the field. I have been CADE trustee from 2010-2011 and from 2014-2020.
I am honored to be nominated for the CADE Board of Trustees. Having joined CADE for the first time in 2011, I am among the younger members of the CADE community. I have been a PC member of IJCAR and CADE and have been involved as a PC member in several conferences related to automated deduction including ITP, FroCoS, CPP, IJCAI, and NeurIPS.
My research is centered around automation for proof assistants, as well as automated reasoning systems based on higher-order logic and type theory. I work both with symbolic approaches and heuristics for sound and complete calculi, as well as with machine learning approaches that may be incomplete but are often able to prove more conjectures in practice.
As a CADE trustee I would support attractive cost-effective open-access options. CADE is already a very open community but I would further welcome automation in the emerging non-classical logics and interdisciplinary applications. I also support the travel awards and best paper awards that make the community more accessible to younger scientists.
Because CADE has exciting research to share, I believe that CADE should be open, welcoming, and first-rate. All CADE publications should be Open Access, because CADE findings are too important to be overlooked by researchers in other fields or with limited library access. The CADE community needs to continue its traditional strength of being particularly warm and welcoming to young researchers. And CADE (along with IJCAR) has to be more widely recognized as the flagship conference in automated reasoning that it is.
Along with my CADE-28 conference co-chair Marijn Heule and PC-co-chair Geoff Sutcliffe, I took a pioneering role in making the CADE-28 proceedings Open Access while I served as conference and PC co-chair. While CADE-28 showed that, with good contacts to publishers and funding sources, Open Access CADE can be cost-effective, CADE still needs a longer-term strategy to balance cost, increase Open Access, but retain or increase CADE publication quality.
CADE is very welcoming to young scientists. But I believe it can do better by investing in the future with an automated reasoning summer school right before CADE. This will enable PhD students to pick up interesting background for the conference and grow into an international young scientists community before the main CADE conference even gets off the ground, which is particularly important to broaden CADE's scope, e.g., in reasoning applications and interdisciplinary research.
I am a passionate believer that deduction is a central significant element of logic, which is why I championed and organized the ACM SIGLOG affiliation of CADE when I co-chaired CADE-28. That is why, alongside LICS and CAV, CADE now has a representation in ACM SIGLOG, which I believe should become CADE's long-term perspective to be heard.
If we play our cards right as a community, then CADE has a strong future ahead.
My background: I am the Alexander von Humboldt Professor for Logic of Autonomous Dynamical Systems at Karlsruhe Institute of Technology (KIT) and lead the Logical Systems Lab at Carnegie Mellon University. My research characterizes the logical foundations of cyber-physical systems and answers the question how we can trust a computer to control physical processes. The solution to this challenge is the key to enabling computer assistance that we can bet our lives on. I pursue this challenge with the principled design of programming languages with logics that can provide proofs as correctness guarantees, such as in our KeYmaera theorem provers.
I have contributed as an author to CADE/IJCAR (where the largest percentage of my papers are published), shared my views on logic and proofs in an invited talk at IJCAR 2016, served on several CADE/IJCAR PCs, and have been co-chair of CADE-28 in 2021. I serve on the editorial board of the Journal of Automated Reasoning, Acta Informatica, and the ACM Formal Aspects of Computing.
I work in automated reasoning since my PhD. CADE and IJCAR are the venues where I feel at home. I have been on the program committee of these conferences in their last two occurrences. Additionally, in 2021 I spammed the world as CADE's publicity chair, and this year I served as IJCAR's workshop co-chair. I am also in the steering committee of PAAR since 2020 and editor of the AAR newsletter since 2017.
My research interests revolve around first- and higher-order classical logic. In particular, now that superposition works in higher-order logic, I want to make higher-order SMT work even better, for which I am looking into higher-order quantifier instantiation. I am also interested in using Isabelle to verify theoretical (AR) results. I would love to see more formally verified AR results at CADE.
I support CADE's recent move to open access and would like its application to be more straightforward. I also believe we should make more efforts concerning reproducible research, e.g. by taking inspiration from venues such as CAV, or by making general-purpose open repositories such as Zenodo mandatory for archival of scripts, binaries and experimental results. In general, I also want to encourage the adoption of implementation guidelines (or good practices) in the community.