Fetching the paper…
Reading the bibliography…
Formal verification provides a rigorous and systematic approach to ensure the correctness and reliability of software systems.
Mining specifications
Glenn Ammons, Rastislav Bodik, and James R Larus · 2002
Earlier work this paper cites.
Automatic generation and checking of program specifications
Jeremy William Nimmer · 2002
Earlier work this paper cites.
Inferring disjunctive postconditions
Corneliu Popeea and Wei-Ngan Chin · 2006
Earlier work this paper cites.
Perracotta: mining temporal api rules from imperfect traces
Jinlin Yang, David Evans, Deepali Bhardwaj, Thirumalesh Bhat, and Manuvir Das · 2006
Earlier work this paper cites.
Efficient mining of iterative patterns for software specification discovery
David Lo, Siau-Cheng Khoo, and Chao Liu · 2007
Earlier work this paper cites.
Static specification inference using predicate mining
Murali Krishna Ramanathan, Ananth Grama, and Suresh Jagannathan · 2007
Earlier work this paper cites.
Static specification mining using automata-based abstractions
Sharon Shoham, Eran Yahav, Stephen Fink, and Marco Pistoia · 2007
Earlier work this paper cites.
Invgen: An efficient invariant generator
Ashutosh Gupta and Andrey Rybalchenko · 2009
Earlier work this paper cites.
Probabilistic, modular and scalable inference of typestate specifications
Nels E Beckman and Aditya V Nori · 2011
Earlier work this paper cites.
Inductive invariant generation via abductive inference
Isil Dillig, Thomas Dillig, Boyang Li, and Ken McMillan · 2013
Earlier work this paper cites.
Automatic inference of necessary preconditions
Patrick Cousot, Radhia Cousot, Manuel Fähndrich, and Francesco Logozzo · 2013
Earlier work this paper cites.
Inductive invariant generation via abductive inference
Isil Dillig, Thomas Dillig, Boyang Li, and Ken McMillan · 2013
Earlier work this paper cites.
A case study on verification of a cloud hypervisor by proof and structural testing
Nikolai Kosmatov, Matthieu Lemerre, and Céline Alec · 2014
Earlier work this paper cites.
Shape analysis via second-order bi-abduction
Quang Loc Le, Cristian Gherghina, Shengchao Qin, and Wei-Ngan Chin · 2014
Earlier work this paper cites.
Frank Dordowsky · 2015
Earlier work this paper cites.
A case study on formal verification of the anaxagoros hypervisor paging system with frama-c
Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, and Frédéeric Loulergue · 2015
Earlier work this paper cites.
Termination and non-termination specification inference
Ton Chanh Le, Shengchao Qin, and Wei-Ngan Chin · 2015
Earlier work this paper cites.
Frama-c: A software analysis perspective
Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski · 2015
Earlier work this paper cites.
Data-driven precondition inference with learned features
Saswat Padhi, Rahul Sharma, and Todd Millstein · 2016
Earlier work this paper cites.
Polynomial invariants by linear algebra
Steven de Oliveira, Saddek Bensalem, and Virgile Prevosto · 2016
Earlier work this paper cites.
Finding polynomial loop invariants for probabilistic programs
Yijun Feng, Lijun Zhang, David N Jansen, Naijun Zhan, and Bican Xia · 2017
Earlier work this paper cites.
Fib: Squeezing loop invariants by interpolation between forward/backward predicate transformers
Shang-Wei Lin, Jun Sun, Hao Xiao, Yang Liu, David Sanán, and Henri Hansen · 2017
Earlier work this paper cites.
Learning loop invariants for program verification
Xujie Si, Hanjun Dai, Mukund Raghothaman, Mayur Naik, and Le Song · 2018
Earlier work this paper cites.
Deductive verification of unmodified linux kernel library functions
Denis Efremov, Mikhail Mandrykin, and Alexey Khoroshilov · 2018
Cited alongside, same era.
Using consensus to automatically infer post-conditions
Jingyi Su, Mohd Arafat, and Robert Dyer · 2018
Cited alongside, same era.
An algorithm and tool to infer practical postconditions
John L Singleton, Gary T Leavens, Hridesh Rajan, and David Cok · 2018
Cited alongside, same era.
Deep specification mining
Tien-Duy B Le and David Lo · 2018
Cited alongside, same era.
Deductive software verification: from pen-and-paper proofs to industrial tools
Reiner Hähnle and Marieke Huisman · 2019
Cited alongside, same era.
Journey to a rte-free x. 509 parser
Arnaud Ebalard, Patricia Mouy, and Ryad Benadjila · 2019
Cited alongside, same era.
Loop invariant inference through smt solving enhanced reinforcement learning
Shiwen Yu, Ting Wang, and Ji Wang · 2023
Later among the works it cites.
OpenAI · 2023
Later among the works it cites.
Lost in the middle: How language models use long contexts
Nelson F Liu, Kevin Lin, John Hewitt, Ashwin Paranjape, Michele Bevilacqua, Fabio Petroni, and Percy Liang · 2023
Later among the works it cites.
How effective are neural networks for fixing security vulnerabilities
Yi Wu, Nan Jiang, Hung Viet Pham, Thibaud Lutellier, Jordan Davis, Lin Tan, Petr Babkin, and Sameena Shah · 2023
Later among the works it cites.
nl2spec: Interactively translating unstructured natural language to temporal logics with large language models
Matthias Cosler, Christopher Hahn, Daniel Mendoza, Frederik Schmitt, and Caroline Trippel · 2023
Later among the works it cites.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Rajeev Alur, Dana Fisman, Saswat Padhi, Rishabh Singh, and Abhishek Udupa · 2019
Cited alongside, same era.
Towards full proof automation in frama-c using auto-active verification
Allan Blanchard, Frédéric Loulergue, and Nikolai Kosmatov · 2019
Cited alongside, same era.
Cln2inv: Learning loop invariants with continuous logic network
Gabriel Ryan, Justin Wong, Jianan Yao, Ronghui Gu, and Suman Jana · 2020
Cited alongside, same era.
Learning nonlinear loop invariants with gated continuous logic networks
Jianan Yao, Gabriel Ryan, Justin Wong, Suman Jana, and Ronghui Gu · 2020
Cited alongside, same era.
Nonlinear craig interpolant generation
Ting Gan, Bican Xia, Bai Xue, Naijun Zhan, and Liyun Dai · 2020
Cited alongside, same era.
Maximum causal entropy specification inference from demonstrations
Marcell Vazquez-Chanlatte and Sanjit A Seshia · 2020
Cited alongside, same era.
Large language models for software engineering: A systematic literature review
Xinyi Hou, Yanjie Zhao, Yue Liu, Zhou Yang, Kailong Wang, Li Li, Xiapu Luo, David Lo, John C. Grundy, and Haoyu Wang · 2023
Later among the works it cites.
Large language models are zero-shot fuzzers: Fuzzing deep-learning libraries via large language models
Yinlin Deng, Chunqiu Steven Xia, Haoran Peng, Chenyuan Yang, and Lingming Zhang · 2023
Later among the works it cites.
Codamosa: Escaping coverage plateaus in test generation with pre-trained large language models
Caroline Lemieux, Jeevana Priya Inala, Shuvendu K. Lahiri, and Siddhartha Sen · 2023
Later among the works it cites.
Automatic code summarization via chatgpt: How far are we?
Weisong Sun, Chunrong Fang, Yudu You, Yun Miao, Yi Liu, Yuekang Li, Gelei Deng, Shenghan Huang, Yuchen Chen, Quanjun Zhang, Hanwei Qian, Yang Liu, and Zhenyu Chen · 2023
Later among the works it cites.
Poster: Assisting static analysis with large language models: A chatgpt experiment
Haonan Li, Yu Hao, Yizhuo Zhai, and Zhiyun Qian · 2023
Later among the works it cites.
Baldur: whole-proof generation and repair with large language models
Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun · 2023
Later among the works it cites.
Lemur: Integrating large language models in automated program verification
Haoze Wu, Clark Barrett, and Nina Narodytska · 2023
Later among the works it cites.
Leandojo: Theorem proving with retrieval-augmented language models
Kaiyu Yang, Aidan M Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar · 2023
Later among the works it cites.
Large language models are few-shot testers: Exploring llm-based general bug reproduction
Sungmin Kang, Juyeon Yoon, and Shin Yoo · 2023
Later among the works it cites.
Examining zero-shot vulnerability repair with large language models
Hammond Pearce, Benjamin Tan, Baleegh Ahmad, Ramesh Karri, and Brendan Dolan-Gavitt · 2023
Later among the works it cites.
Automated program repair in the era of large pre-trained language models
Chunqiu Steven Xia, Yuxiang Wei, and Lingming Zhang · 2023
Later among the works it cites.
Automated repair of programs from large language models
Zhiyu Fan, Xiang Gao, Martin Mirchev, Abhik Roychoudhury, and Shin Hwei Tan · 2023
Later among the works it cites.
The scope of chatgpt in software engineering: A thorough investigation
Wei Ma, Shangqing Liu, Wenhan Wang, Qiang Hu, Ye Liu, Cen Zhang, Liming Nie, and Yang Liu · 2023
Later among the works it cites.
Can large language models reason about program invariants?
Kexin Pei, David Bieber, Kensen Shi, Charles Sutton, and Pengcheng Yin · 2023
Later among the works it cites.
Frama-c, software analzer, Accessed: 2024-01-15
Frama-C · 2024
Closest in time.
A repository dedicated for problems related to verification of programs using the tool frama-c
Frama-C · 2024
Closest in time.
a rte-free x.509 parser, Accessed: 2024-01-15
2024
Closest in time.
Automatically inspecting thousands of static bug warnings with large language model: How far are we?
Cheng Wen, Yuandao Cai, Bin Zhang, Jie Su, Zhiwu Xu, Dugang Liu, Shengchao Qin, Zhong Ming, and Cong Tian · 2024
Closest in time.