Movatterモバイル変換

[0]ホーム
URL:

Skip to main content

Advertisement

Springer Nature Link
Log in

satabs: A Bit-Precise Verifier for C Programs

(Competition Contribution)

  • Conference paper

Abstract

satAbs is a bit-precise software model checker for ANSI-C programs. It implements sound predicate-abstraction based algorithms for both sequential and concurrent software.

This research is supported by EPSRC projects EP/G026254/1, EP/G051100/1 and EP/H017585/1 and ERC project 280053.

Similar content being viewed by others

References

  1. Ball, T., Cook, B., Das, S., Rajamani, S.K.: Refining Approximations in Software Predicate Abstraction. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 388–403. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  2. Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: PLDI, pp. 203–213 (2001)

    Google Scholar 

  3. Basler, G., Hague, M., Kroening, D., Ong, C.-H.L., Wahl, T., Zhao, H.:Boom: Taking Boolean Program Model Checking One Step Further. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 145–149. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  4. Basler, G., Mazzucchi, M., Wahl, T., Kroening, D.: Context-aware counter abstraction. Formal Methods in System Design 36(3), 223–245 (2010)

    Article MATH  Google Scholar 

  5. Clarke, E., Kroning, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  6. Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI–C programs using SAT. Formal Methods in System Design (FMSD) 25, 105–127 (2004)

    Article MATH  Google Scholar 

  7. Clarke, E., Kroning, D., Sharygina, N., Yorav, K.: SATABS: SAT-Based Predicate Abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 570–574. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  8. Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)

    Article MathSciNet  Google Scholar 

  9. Das, S., Dill, D.L.: Successive approximation of abstract transition relations. In: LICS (2001)

    Google Scholar 

  10. Donaldson, A., Kaiser, A., Kroening, D., Wahl, T.: Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 356–371. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  11. Eén, N., Sörensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  12. Graf, S., Saïdi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  13. Wahl, T., Donaldson, A.F.: Replication and abstraction: Symmetry in automated formal verification. Symmetry 2(2), 799–847 (2010)

    Article MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Imperial College, London, United Kingdom

    Gérard Basler & Alastair Donaldson

  2. University of Oxford, United Kingdom

    Alexander Kaiser, Daniel Kroening & Michael Tautschnig

  3. Northeastern University, Boston, USA

    Thomas Wahl

Authors
  1. Gérard Basler

    You can also search for this author inPubMed Google Scholar

  2. Alastair Donaldson

    You can also search for this author inPubMed Google Scholar

  3. Alexander Kaiser

    You can also search for this author inPubMed Google Scholar

  4. Daniel Kroening

    You can also search for this author inPubMed Google Scholar

  5. Michael Tautschnig

    You can also search for this author inPubMed Google Scholar

  6. Thomas Wahl

    You can also search for this author inPubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of California at Santa Cruz, 1156 High Street, 95064, Santa Cruz, CA, USA

    Cormac Flanagan

  2. Fakultät für Ingenieurwesen, Abteilung für Informatik und Angewandte Kognitionswissenschaft, Universität Duisburg-Essen, Lotharstraße 65, 47057, Duisburg, Germany

    Barbara König

Rights and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Basler, G., Donaldson, A., Kaiser, A., Kroening, D., Tautschnig, M., Wahl, T. (2012).satabs: A Bit-Precise Verifier for C Programs. In: Flanagan, C., König, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2012. Lecture Notes in Computer Science, vol 7214. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28756-5_47

Download citation

Publish with us

[8]ページ先頭
©2009-2025 Movatter.jp