\input zb-basic
\input zb-ioport
\iteman{io-port 06109368}
\itemau{Furia, Carlo A.}
\itemti{A verifier for functional properties of sequence-manipulating programs.}
\itemso{Chakraborty, Supratik (ed.) et al., Automated technology for verification and analysis. 10th international symposium, ATVA 2012, Thiruvananthapuram, India, October 3--6, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-33385-9/pbk). Lecture Notes in Computer Science 7561, 183-186 (2012).}
\itemab
Summary: Many programs operate on data structures whose models are sequences, such as arrays, lists, and queues. When specifying and verifying functional properties of such programs, it is convenient to use an assertion language and a reasoning engine that incorporate sequences natively. This paper presents `qfis', a program verifier geared to sequence-manipulating programs. `qfis' is a command-line tool that inputs annotated programs, generates the verification conditions that establish their correctness, tries to discharge them by calls to the SMT-solver CVC3, and reports the outcome back to the user. `qfis' can be used directly or as a back-end of more complex programming languages.
\itemrv{~}
\itemcc{}
\itemut{}
\itemli{doi:10.1007/978-3-642-33386-6\_15}
\end