Добірка наукової літератури з теми "Computer software Verification"
Оформте джерело за APA, MLA, Chicago, Harvard та іншими стилями
Ознайомтеся зі списками актуальних статей, книг, дисертацій, тез та інших наукових джерел на тему "Computer software Verification".
Біля кожної праці в переліку літератури доступна кнопка «Додати до бібліографії». Скористайтеся нею – і ми автоматично оформимо бібліографічне посилання на обрану працю в потрібному вам стилі цитування: APA, MLA, «Гарвард», «Чикаго», «Ванкувер» тощо.
Також ви можете завантажити повний текст наукової публікації у форматі «.pdf» та прочитати онлайн анотацію до роботи, якщо відповідні параметри наявні в метаданих.
Статті в журналах з теми "Computer software Verification":
Goerigk, Wolfgang. "Mechanical Software Verification." Electronic Notes in Theoretical Computer Science 58, no. 2 (November 2001): 117–37. http://dx.doi.org/10.1016/s1571-0661(04)00282-8.
Kwiatkowska, Marta. "From software verification to ‘everyware’ verification." Computer Science - Research and Development 28, no. 4 (September 7, 2013): 295–310. http://dx.doi.org/10.1007/s00450-013-0249-1.
Dobrescu, Mihai, and Katerina Argyraki. "Software dataplane verification." Communications of the ACM 58, no. 11 (October 23, 2015): 113–21. http://dx.doi.org/10.1145/2823400.
Malkis, Alexander, and Anindya Banerjee. "Verification of software barriers." ACM SIGPLAN Notices 47, no. 8 (September 11, 2012): 313–14. http://dx.doi.org/10.1145/2370036.2145871.
Halpern, J. D., S. Owre, N. Proctor, and W. F. Wilson. "Muse—A Computer Assisted Verification System." IEEE Transactions on Software Engineering SE-13, no. 2 (February 1987): 151–56. http://dx.doi.org/10.1109/tse.1987.226477.
Flanagan, Cormac, and Shaz Qadeer. "Predicate abstraction for software verification." ACM SIGPLAN Notices 37, no. 1 (January 2002): 191–202. http://dx.doi.org/10.1145/565816.503291.
Greengard, Samuel. "Formal software verification measures up." Communications of the ACM 64, no. 7 (July 2021): 13–15. http://dx.doi.org/10.1145/3464933.
Andersen, B. Scott, and George Romanski. "Verification of safety-critical software." Communications of the ACM 54, no. 10 (October 2011): 52–57. http://dx.doi.org/10.1145/2001269.2001286.
Andersen, B. Scott, and George Romanski. "Verification of Safety-critical Software." Queue 9, no. 8 (August 2011): 50–59. http://dx.doi.org/10.1145/2016036.2024356.
Hailpern, B., and P. Santhanam. "Software debugging, testing, and verification." IBM Systems Journal 41, no. 1 (2002): 4–12. http://dx.doi.org/10.1147/sj.411.0004.
Дисертації з теми "Computer software Verification":
Dimovski, Aleksandar. "Compositional software verification based on game semantics." Thesis, University of Warwick, 2007. http://wrap.warwick.ac.uk/2398/.
Addy, Edward A. "Verification and validation in software product line engineering." Morgantown, W. Va. : [West Virginia University Libraries], 1999. http://etd.wvu.edu/templates/showETD.cfm?recnum=1068.
Title from document title page. Document formatted into pages; contains vi, 75 p. : ill. (some col.). Includes abstract. Includes bibliographical references (p. 35-39).
Wahab, Matthew. "Object code verification." Thesis, University of Warwick, 1998. http://wrap.warwick.ac.uk/61068/.
Swart, Riaan. "A language to support verification of embedded software." Thesis, Stellenbosch : Stellenbosch University, 2004. http://hdl.handle.net/10019.1/49823.
ENGLISH ABSTRACT: Embedded computer systems form part of larger systems such as aircraft or chemical processing facilities. Although testing and debugging of such systems are difficult, reliability is often essential. Development of embedded software can be simplified by an environment that limits opportunities for making errors and provides facilities for detection of errors. We implemented a language and compiler that can serve as basis for such an experimental environment. Both are designed to make verification of implementations feasible. Correctness and safety were given highest priority, but without sacrificing efficiency wherever possible. The language is concurrent and includes measures for protecting the address spaces of concurrently running processes. This eliminates the need for expensive run-time memory protection and will benefit resource-strapped embedded systems. The target hardware is assumed to provide no special support for concurrency. The language is designed to be small, simple and intuitive, and to promote compile-time detection of errors. Facilities for abstraction, such as modules and abstract data types support implementation and testing of bigger systems. We have opted for model checking as verification technique, so our implementation language is similar in design to a modelling language for a widely used model checker. Because of this, the implementation code can be used as input for a model checker. However, since the compiler can still contain errors, there might be discrepancies between the implementation code written in our language and the executable code produced by the compiler. Therefore we are attempting to make verification of executable code feasible. To achieve this, our compiler generates code in a special format, comprising a transition system of uninterruptible actions. The actions limit the scheduling points present in processes and reduce the different interleavings of process code possible in a concurrent system. Requirements that conventional hardware places on this form of code are discussed, as well as how the format influences efficiency and responsiveness.
AFRIKAANSE OPSOMMING: Ingebedde rekenaarstelsels maak deel uit van groter stelsels soos vliegtuie of chemiese prosesseerfasiliteite. Hoewel toetsing en ontfouting van sulke stelsels moeilik is, is betroubaarheid dikwels onontbeerlik. Ontwikkeling van ingebedde sagteware kan makliker gemaak word met 'n ontwikkelingsomgewing wat geleenthede vir foutmaak beperk en fasiliteite vir foutbespeuring verskaf. Ons het 'n programmeertaal en vertaler geïmplementeer wat as basis kan dien vir so 'n eksperimentele omgewing. Beide is ontwerp om verifikasie van implementasies haalbaar te maak. Korrektheid en veiligheid het die hoogste prioriteit geniet, maar sonder om effektiwiteit prys te gee, waar moontlik. Die taal is gelyklopend en bevat maatreëls om die adresruimtes van gelyklopende prosesse te beskerm. Dit maak duur looptyd-geheuebeskerming onnodig, tot voordeel van ingebedde stelsels met 'n tekort aan hulpbronne. Daar word aangeneem dat die teikenhardeware geen spesiale ondersteuning vir gelyklopendheid bevat nie. Die programmeertaal is ontwerp om klein, eenvoudig en intuïtief te wees, en om vertaaltyd-opsporing van foute te bevorder. Fasiliteite vir abstraksie, byvoorbeeld modules en abstrakte datatipes, ondersteun implementering en toetsing van groter stelsels. Ons het modeltoetsing as verifikasietegniek gekies, dus is die ontwerp van ons programmeertaal soortgelyk aan dié van 'n modelleertaal vir 'n modeltoetser wat algemeen gebruik word. As gevolg hiervan kan die implementasiekode as toevoer vir 'n modeltoetser gebruik word. Omdat die vertaler egter steeds foute kan bevat, mag daar teenstrydighede bestaan tussen die implementasie geskryf in ons implementasietaal, en die uitvoerbare masjienkode wat deur die vertaler gelewer word. Daarom poog ons om verifikasie van die uitvoerbare masjienkode haalbaar te maak. Om hierdie doelwit te bereik, is ons vertaler ontwerp om 'n spesiale formaat masjienkode te genereer bestaande uit 'n oorgangstelsel wat ononderbreekbare (atomiese) aksies bevat. Die aksies beperk die skeduleerpunte in prosesse en verminder sodoende die aantal interpaginasies van proseskode wat moontlik is in 'n gelyklopende stelsel. Die vereistes wat konvensionele hardeware aan dié spesifieke formaat kode stel, word bespreek, asook hoe die formaat effektiwiteit en reageerbaarheid van die stelsel beïnvloed.
Wang, Xuan. "Verification of Digital Controller Verifications." BYU ScholarsArchive, 2005. https://scholarsarchive.byu.edu/etd/681.
Tagore, Aditi. "Techniques to Improve Automated Software Verification." The Ohio State University, 2014. http://rave.ohiolink.edu/etdc/view?acc_num=osu1397661277.
Kirschenbaum, Jason P. "Investigations in Automating Software Verification." The Ohio State University, 2011. http://rave.ohiolink.edu/etdc/view?acc_num=osu1306862918.
Hughes, Roger Brett. "Automated interactive software verification and synthesis." Thesis, Brunel University, 1992. http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.306741.
Jackson, David Mark. "Logical verification of reactive software systems." Thesis, University of Oxford, 1992. http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.305989.
Ibrahim, Alaa E. "Scenario-based verification and validation of dynamic UML specifications." Morgantown, W. Va. : [West Virginia University Libraries], 2001. http://etd.wvu.edu/templates/showETD.cfm?recnum=1799.
Title from document title page. Document formatted into pages; contains x, 143 p. : ill. (some col.). Vita. Includes abstract. Includes bibliographical references (p. 96-99).
Книги з теми "Computer software Verification":
1943-, Kurshan R. P., ed. Computer-aided verification. Boston: Kluwer Academic Publishers, 1992.
Nissim, Francez. Program verification. Wokingham, Eng: Addison-Wesley Pub. Co., 1992.
Nachum, Dershowitz, and Manna Zohar, eds. Verification: Theory and practice : essays dedicated to Zohar Manna on the occasion of his 64th birthday. Berlin: Springer-Verlag, 2004.
Apt, Krzysztof R. Verification of sequential and concurrent programs. New York: Springer-Verlag, 1991.
Apt, Krzysztof R. Verification of sequential and concurrent programs. 2nd ed. New York: Springer-Verlag, 1997.
1952-, Colburn Timothy R., Fetzer James H. 1940-, and Rankin Terry L, eds. Program verification: Fundamental issues in computer science. Dordrecht: Kluwer Academic Publishers, 1993.
Almeida, José Bacelar. Rigorous software development: An introduction to program verification. London: Springer, 2011.
Bergé, Jean-Michel. Hardware/Software Co-Design and Co-Verification. Boston, MA: Springer US, 1997.
Jean-Michel, Bergé, Levia Oz, and Rouillard Jacques, eds. Hardware/software co-design and co-verification. Boston: Kluwer Academic Publishers, 1997.
Hoare, C. A. R., M. Broy, and Christian Leuxner. Software and systems safety: Specification and verification. Amsterdam: IOS Press, 2011.
Частини книг з теми "Computer software Verification":
Revesz, Peter. "Software Verification." In Texts in Computer Science, 685–99. London: Springer London, 2009. http://dx.doi.org/10.1007/978-1-84996-095-3_26.
Weik, Martin H. "software verification." In Computer Science and Communications Dictionary, 1611. Boston, MA: Springer US, 2000. http://dx.doi.org/10.1007/1-4020-0613-6_17667.
Peled, Doron A. "Deductive Software Verification." In Texts in Computer Science, 179–213. New York, NY: Springer New York, 2001. http://dx.doi.org/10.1007/978-1-4757-3540-6_7.
Weik, Martin H. "automated software verification." In Computer Science and Communications Dictionary, 81. Boston, MA: Springer US, 2000. http://dx.doi.org/10.1007/1-4020-0613-6_1068.
Cimatti, Alessandro, and Alberto Griggio. "Software Model Checking via IC3." In Computer Aided Verification, 277–93. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012. http://dx.doi.org/10.1007/978-3-642-31424-7_23.
Hoare, Tony. "The Ideal of Verified Software." In Computer Aided Verification, 5–16. Berlin, Heidelberg: Springer Berlin Heidelberg, 2006. http://dx.doi.org/10.1007/11817963_4.
Holzmann, Gerard_J. "Software Analysis and Model Checking." In Computer Aided Verification, 1–16. Berlin, Heidelberg: Springer Berlin Heidelberg, 2002. http://dx.doi.org/10.1007/3-540-45657-0_1.
Cousot, Patrick, and Radhia Cousot. "On Abstraction in Software Verification." In Computer Aided Verification, 37–56. Berlin, Heidelberg: Springer Berlin Heidelberg, 2002. http://dx.doi.org/10.1007/3-540-45657-0_3.
Ivančić, F., Z. Yang, M. K. Ganai, A. Gupta, I. Shlyakhter, and P. Ashar. "F-Soft: Software Verification Platform." In Computer Aided Verification, 301–6. Berlin, Heidelberg: Springer Berlin Heidelberg, 2005. http://dx.doi.org/10.1007/11513988_31.
van der Berg, Freark I. "LLMC: Verifying High-Performance Software." In Computer Aided Verification, 690–703. Cham: Springer International Publishing, 2021. http://dx.doi.org/10.1007/978-3-030-81688-9_32.
Тези доповідей конференцій з теми "Computer software Verification":
Usener, Claus A., Susanne Gruttmann, Tim A. Majchrzak, and Herbert Kuchen. "Computer-Supported Assessment of Software Verification Proofs." In 2010 International Conference on Educational and Information Technology (ICEIT). IEEE, 2010. http://dx.doi.org/10.1109/iceit.2010.5607766.
Mukherjee, Rajdeep, Daniel Kroening, and Tom Melham. "Hardware Verification Using Software Analyzers." In 2015 IEEE Computer Society Annual Symposium on VLSI (ISVLSI). IEEE, 2015. http://dx.doi.org/10.1109/isvlsi.2015.107.
Asadollahi, Somayeh, Vahid Rafe, and Reza Rafeh. "Towards Automated Software Verification and Validation." In 2009 International Conference on Computer Technology and Development. IEEE, 2009. http://dx.doi.org/10.1109/icctd.2009.164.
Grimm, Tomas, Djones Lettnin, and Michael Hubner. "Semiformal Verification of Software-Controlled Connections." In 2017 IEEE Computer Society Annual Symposium on VLSI (ISVLSI). IEEE, 2017. http://dx.doi.org/10.1109/isvlsi.2017.103.
Biswas, M. A. Rafe, Samuel Garcia, Matthew Prado, Sadad Hossain, Matthew Souris, and Lee Morin. "Software verification of Orion cockpit displays." In 2017 12th International Conference on Computer Science and Education (ICCSE). IEEE, 2017. http://dx.doi.org/10.1109/iccse.2017.8085474.
Cruz, Daniela da, Pedro Rangel Henriques, and Jorge Sousa Pinto. "Interactive Verification of Safety-Critical Software." In 2013 IEEE 37th Annual Computer Software and Applications Conference (COMPSAC). IEEE, 2013. http://dx.doi.org/10.1109/compsac.2013.86.
Chao Wang, Malay Ganai, Shuvendu Lahiri, and Daniel Kroening. "Embedded software verification: Challenges and solutions." In 2008 IEEE/ACM International Conference on Computer-Aided Design (ICCAD). IEEE, 2008. http://dx.doi.org/10.1109/iccad.2008.4681536.
Ding Zheng, Yichen Wang, and Zou Xueyi. "The methods of FPGA software verification." In 2011 IEEE International Conference on Computer Science and Automation Engineering (CSAE). IEEE, 2011. http://dx.doi.org/10.1109/csae.2011.5952639.
Craig, D. C., and W. M. Zuberek. "Compatibility of Software Components - Modeling and Verification." In 2006 International Conference on Dependability of Computer Systems. IEEE, 2006. http://dx.doi.org/10.1109/depcos-relcomex.2006.13.
Lettnin, Djones, Markus Winterholer, Axel Braun, Joachim Gerlach, Jurgen Ruf, Thomas Kropf, and Wolfgang Rosenstiel. "Coverage Driven Verification applied to Embedded Software." In IEEE Computer Society Annual Symposium on VLSI (ISVLSI '07). IEEE, 2007. http://dx.doi.org/10.1109/isvlsi.2007.33.