Fetching the paper…
Reading the bibliography…
Formal program specifications play a crucial role in various stages of software development.
P. A. Abdulla and B. Jonsson, “Undecidable verification problems for programs with unreliable channels,” Information and Computation , vol. 130, no. 1, pp. 71–90, 1996
1996
Earlier work this paper cites.
C. Flanagan and K. R. M. Leino, “Houdini, an annotation assistant for esc/java,” in International Symposium of Formal Methods Europe . Springer, 2001, pp. 500–517
2001
Earlier work this paper cites.
C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata, “Extended static checking for java,” in Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation , 2002, pp. 234–245
2002
Earlier work this paper cites.
J. W. Nimmer and M. D. Ernst, “Automatic generation of program specifications,” ACM SIGSOFT Software Engineering Notes , vol. 27, no. 4, pp. 229–239, 2002
2002
Earlier work this paper cites.
E. Rodríguez-Carbonell and D. Kapur, “Program verification using automatic generation of invariants,” in International Colloquium on Theoretical Aspects of Computing . Springer, 2004, pp. 325–340
2004
Earlier work this paper cites.
L. Burdy, Y. Cheon, D. R. Cok, M. D. Ernst, J. R. Kiniry, G. T. Leavens, K. R. M. Leino, and E. Poll, “An overview of jml tools and applications,” International journal on software tools for technology transfer , vol. 7, pp. 212–232, 2005
2005
Earlier work this paper cites.
W. Ahrendt, T. Baar, B. Beckert, R. Bubel, M. Giese, R. Hähnle, W. Menzel, W. Mostowski, A. Roth, S. Schlager et al. , “The key tool: integrating object oriented design and formal verification,” Software & Systems Modeling , vol. 4, pp. 32–54, 2005
2005
Earlier work this paper cites.
M. D. Ernst, J. H. Perkins, P. J. Guo, S. McCamant, C. Pacheco, M. S. Tschantz, and C. Xiao, “The daikon system for dynamic detection of likely invariants,” Science of computer programming , vol. 69, no. 1-3, pp. 35–45, 2007
2007
Earlier work this paper cites.
M. Christodorescu, S. Jha, and C. Kruegel, “Mining specifications of malicious behavior,” in Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering , 2007, pp. 5–14
2007
Earlier work this paper cites.
G. Cabodi, S. Nocco, and S. Quer, “Strengthening model checking techniques with inductive invariants,” IEEE transactions on computer-aided design of integrated circuits and systems , vol. 28, no. 1, pp. 154–158, 2008
2008
Earlier work this paper cites.
E. I. Leonard and C. L. Heitmeyer, “Automatic program generation from formal specifications using apts,” Automatic Program Development: A Tribute to Robert Paige , pp. 93–113, 2008
2008
Earlier work this paper cites.
M. Pradel and T. R. Gross, “Automatic generation of object usage specifications from large method traces,” in 2009 IEEE/ACM International Conference on Automated Software Engineering . IEEE, 2009, pp. 371–382
2009
Earlier work this paper cites.
Y. Moy and C. Marché, “Modular inference of subprogram contracts for safety checking,” Journal of Symbolic Computation , vol. 45, no. 11, pp. 1184–1211, 2010
2010
Earlier work this paper cites.
Y. Wei, C. A. Furia, N. Kazmin, and B. Meyer, “Inferring better contracts,” in Proceedings of the 33rd International Conference on Software Engineering , 2011, pp. 191–200
2011
Earlier work this paper cites.
D. R. Cok, “Openjml: Jml for java 7 by extending openjdk,” in NASA Formal Methods: Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings 3 . Springer, 2011, pp. 472–479
2011
Earlier work this paper cites.
A. Mesbah, A. van Deursen, and D. Roest, “Invariant-based automatic testing of modern web applications,” IEEE Transactions on Software Engineering , vol. 38, no. 1, pp. 35–53, 2012
2012
Earlier work this paper cites.
F. Aarts, F. Heidarian, H. Kuppens, P. Olsen, and F. Vaandrager, “Automata learning through counterexample guided abstraction refinement,” in FM 2012: Formal Methods: 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings 18 . Springer, 2012, pp. 10–27
2012
Earlier work this paper cites.
P. Cousot, R. Cousot, M. Fähndrich, and F. Logozzo, “Automatic inference of necessary preconditions,” in International Workshop on Verification, Model Checking, and Abstract Interpretation . Springer, 2013, pp. 128–148
2013
Earlier work this paper cites.
F. Rahman and Y. Labiche, “A comparative study of invariants generated by daikon and user-defined design contracts,” in 2014 14th International Conference on Quality Software . IEEE, 2014, pp. 174–183
2014
Earlier work this paper cites.
T. Nemoto and D. Beglar, “Likert-scale questionnaires,” in JALT 2013 conference proceedings , 2014, pp. 1–8
2014
Earlier work this paper cites.
R. Just, D. Jalali, and M. D. Ernst, “Defects4j: A database of existing faults to enable controlled testing studies for java programs,” in Proceedings of the 2014 international symposium on software testing and analysis , 2014, pp. 437–440
2014
Earlier work this paper cites.
D. Beyer, M. Dangl, and P. Wendler, “Boosting k-induction with continuously-refined invariants,” in International Conference on Computer Aided Verification . Springer, 2015, pp. 622–640
2015
Earlier work this paper cites.
P. Garg, D. Neider, P. Madhusudan, and D. Roth, “Learning invariants using decision trees and implication counterexamples,” ACM Sigplan Notices , vol. 51, no. 1, pp. 499–512, 2016
2016
Earlier work this paper cites.
X. Xie, B. Chen, L. Zou, Y. Liu, W. Le, and X. Li, “Automatic loop summarization via path dependency analysis,” IEEE Transactions on Software Engineering , vol. 45, no. 6, pp. 537–557, 2017
2017
Earlier work this paper cites.
V. Murali, S. Chaudhuri, and C. Jermaine, “Bayesian specification learning for finding api usage errors,” in Proceedings of the 2017 11th joint meeting on foundations of software engineering , 2017, pp. 151–162
2017
Earlier work this paper cites.
C. Barrett and C. Tinelli, Satisfiability modulo theories . Springer, 2018
2018
Earlier work this paper cites.
2018
Earlier work this paper cites.
X. Si, H. Dai, M. Raghothaman, M. Naik, and L. Song, “Learning loop invariants for program verification,” Advances in Neural Information Processing Systems , vol. 31, 2018
2018
Cited alongside, same era.
Z. Y. Ding, Y. Lyu, C. Timperley, and C. Le Goues, “Leveraging program invariants to promote population diversity in search-based automatic program repair,” in 2019 IEEE/ACM International Workshop on Genetic Improvement (GI) . IEEE, 2019, pp. 2–9
2019
Cited alongside, same era.
2019
Cited alongside, same era.
2019
Cited alongside, same era.
2023
Later among the works it cites.
2023
Later among the works it cites.
Y. Wei, C. S. Xia, and L. Zhang, “Copiloting the copilots: Fusing large language models with completion engines for automated program repair,” in Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering , 2023, pp. 172–184
2023
Later among the works it cites.
2023
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
2019
Cited alongside, same era.
T. Brown, B. Mann, N. Ryder, M. Subbiah, J. D. Kaplan, P. Dhariwal, A. Neelakantan, P. Shyam, G. Sastry, A. Askell et al. , “Language models are few-shot learners,” Advances in neural information processing systems , vol. 33, pp. 1877–1901, 2020
2020
Cited alongside, same era.
A. Alshnakat, D. Gurov, C. Lidström, and P. Rümmer, “Constraint-based contract inference for deductive verification,” Deductive Software Verification: Future Perspectives: Reflections on the Occasion of 20 Years of KeY , pp. 149–176, 2020
2020
Cited alongside, same era.
U. Mathur, P. Madhusudan, and M. Viswanathan, “What’s decidable about program verification modulo axioms?” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems . Springer, 2020, pp. 158–177
2020
Cited alongside, same era.
2020
Cited alongside, same era.
2020
Cited alongside, same era.
V. Terragni, G. Jahangirova, P. Tonella, and M. Pezzè, “Evolutionary improvement of assertion oracles,” in Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering , 2020, pp. 1178–1189
2020
Cited alongside, same era.
2021
Cited alongside, same era.
Later among the works it cites.
2023
Later among the works it cites.
OpenAI, “Gpt-4 technical report,” 2023
2023
Later among the works it cites.
——, “Api reference - openai api,” 2023, https://platform.openai.com/docs/api-reference
2023
Later among the works it cites.
LeetCode, “The world’s leading online programming learning platform,” 2023, https://leetcode.com/
2023
Later among the works it cites.
Parasoft, “Ai-powered java testing tool,” 2023, https://www.parasoft.com/products/parasoft-jtest/
2023
Later among the works it cites.
Microsoft, “Code contracts - microsoft research,” 2023, https://www.microsoft.com/en-us/research/project/code-contracts/
2023
Later among the works it cites.
S. Ghosal, B. Jonsson, and P. Rümmer, “An active learning approach to synthesizing program contracts,” in International Conference on Software Engineering and Formal Methods . Springer, 2023, pp. 126–144
2023
Later among the works it cites.
2023
Later among the works it cites.
P. Liu, W. Yuan, J. Fu, Z. Jiang, H. Hayashi, and G. Neubig, “Pre-train, prompt, and predict: A systematic survey of prompting methods in natural language processing,” ACM Computing Surveys , vol. 55, no. 9, pp. 1–35, 2023
2023
Later among the works it cites.
B. Min, H. Ross, E. Sulem, A. P. B. Veyseh, T. H. Nguyen, O. Sainz, E. Agirre, I. Heintz, and D. Roth, “Recent advances in natural language processing via large pre-trained language models: A survey,” ACM Computing Surveys , vol. 56, no. 2, pp. 1–40, 2023
2023
Later among the works it cites.
S. Hegselmann, A. Buendia, H. Lang, M. Agrawal, X. Jiang, and D. Sontag, “Tabllm: Few-shot classification of tabular data with large language models,” in Proceedings of The 26th International Conference on Artificial Intelligence and Statistics , ser. Proceedings of Machine Learning Research, F. Ruiz, J. Dy, and J.-W. van de Meent, Eds., vol. 206. PMLR, 25–27 Apr 2023, pp. 5549–5581. [Online]. Available: https://proceedings.mlr.press/v206/hegselmann23a.html
2023
Later among the works it cites.
2023
Later among the works it cites.
2023
Later among the works it cites.
2023
Later among the works it cites.
2023
Later among the works it cites.
2023
Later among the works it cites.
K. Pei, D. Bieber, K. Shi, C. Sutton, and P. Yin, “Can large language models reason about program invariants?” in International Conference on Machine Learning . PMLR, 2023, pp. 27 496–27 520
2023
Later among the works it cites.
sosy lab, “Sv-comp - international competition on software verification,” 2024, https://sites.google.com/view/specgen
2024
Closest in time.
2024
Closest in time.
Github, “Specgen-artifact,” 2024, https://github.com/Lezhi-Ma/SpecGen-Artifact
2024
Closest in time.
EclEmma, “Eclemma - jacoco java code coverage library,” 2024, https://www.eclemma.org/jacoco/
2024
Closest in time.
S. Iyer, I. Konstas, A. Cheung, and L. Zettlemoyer, “Summarizing source code using a neural attention model,” in 54th Annual Meeting of the Association for Computational Linguistics 2016 . Association for Computational Linguistics, 2016, pp. 2073–2083
2083
Closest in time.