Bit-precise procedure-modular termination analysis
Non-termination is the root cause of a variety of program bugs, such as hanging programs and vulnerabilities to denial-of-service attacks. This makes an automated analysis that can prove the absence of such bugs highly desirable. To scale termination checks to large systems, an interprocedural termi...
Main Authors: | Chen, H, David, C, Kroening, D, Schrammel, P, Wachter, B |
---|---|
Format: | Journal article |
Published: |
Association for Computing Machinery
2018
|
Similar Items
-
Synthesising interprocedural bit-precise termination proofs
by: Chen, H, et al.
Published: (2016) -
Unrestricted termination and non-termination arguments for bit-vector programs
by: David, C, et al.
Published: (2015) -
Sound static deadlock analysis for C/Pthreads
by: Kroening, D, et al.
Published: (2016) -
Sound static deadlock analysis for C/Pthreads (extended version)
by: Kroening, D, et al.
Published: (2016) -
Ranking function synthesis for bit-vector relations
by: Cook, B, et al.
Published: (2010)