program verification - researchr tag

researchr

You are not signed in
Sign in
Sign up

2012

SAFECOMP, Proceedings2012.

2011

Streaming transducers for algorithmic verification of single-pass list-processing programsRajeev Alur, Pavol Cerný. POPL 2011: 599-610 [doi]

Relational Verification Using Product ProgramsGilles Barthe, Juan Manuel Crespo, César Kunz. fm 2011: 200-214 [doi]

Verifying Object-Oriented Programs with Higher-Order Separation Logic in CoqJesper Bengtson, Jonas Braband Jensen, Filip Sieczkowski, Lars Birkedal. itp 2011: 22-38 [doi]

Verifying stateful programs with substructural state and hoare typesJohannes Borgström, Juan Chen, Nikhil Swamy. plpv 2011: 15-26 [doi]

Infer: An Automatic Program Verifier for Memory Safety of C ProgramsCristiano Calcagno, Dino Distefano. NFM 2011: 459-465 [doi]

CleanJava: A Formal Notation for Functional Program VerificationYoonsik Cheon, Cesar Yeep, Melisa Vela. itng 2011: 221-226 [doi]

Temporal Property Verification as a Program Analysis TaskByron Cook, Eric Koskinen, Moshe Y. Vardi. cav 2011: 333-348 [doi]

An innovative teaching tool based on semantic tableaux for verification and debugging of programsRafael del Vado Vírseda, Fernando Pérez Morente. iticse 2011: 352 [doi]

An Innovative Teaching Tool based on Semantic Tableaux for Verification and Debugging of Imperative ProgramsRafael del Vado Vírseda, Fernando Pérez Morente. procedia, 4:1907-1916, 2011. [doi]

System Verification through Program VerificationDaniel Dietsch, Bernd Westphal, Andreas Podelski. fm 2011: 27-41 [doi]

Complexity of pattern-based verification for multithreaded programsJavier Esparza, Pierre Ganty. POPL 2011: 499-510 [doi]

Program transformation for development, verification, and synthesis of programsFabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Valerio Senni. ia, 5(1):119-125, 2011. [doi]

On-Device Control Flow Verification for Java ProgramsArnaud Fontaine, Samuel Hym, Isabelle Simplot-Ryl. ESSoS 2011: 43-57 [doi]

Verification conditions for source-level imperative programsMaria João Frade, Jorge Sousa Pinto. csr, 5(3):252-277, 2011. [doi]

Verified Synthesis of Knowledge-Based Programs in Finite Synchronous EnvironmentsPeter Gammie. itp 2011: 87-102 [doi]

Structured Specifications for Better Verification of Heap-Manipulating ProgramsCristian Gherghina, Cristina David, Shengchao Qin, Wei-Ngan Chin. fm 2011: 386-401 [doi]

Predicate abstraction and refinement for verifying multi-threaded programsAshutosh Gupta, Corneliu Popeea, Andrey Rybalchenko. POPL 2011: 331-344 [doi]

Threader: A Constraint-Based Verifier for Multi-threaded ProgramsAshutosh Gupta, Corneliu Popeea, Andrey Rybalchenko. cav 2011: 412-417 [doi]

HMC: Verifying Functional Programs Using Abstract InterpretersRanjit Jhala, Rupak Majumdar, Andrey Rybalchenko. cav 2011: 470-485 [doi]

Proceedings of the 5th ACM Workshop Programming Languages meets Program Verification, PLPV 2011, Austin, TX, USA, January 29, 2011Ranjit Jhala, Wouter Swierstra, editors, ACM, 2011.

Brief announcement: program regularization in verifying memory consistencyLei Li, Tianshi Chen, Yunji Chen, Ling Li, Cheng Qian, Weiwu Hu. spaa 2011: 265-266 [doi]

UML interaction model-driven runtime verification of Java programsX. Li, X. Qiu, L. Wang, X. Chen, Z. Zhou, L. Yu, J. Zhao. iee, 5(2):142-156, 2011. [doi]

Trace-based verification of imperative programs with I/OGregory Malecha, Greg Morrisett, Ryan Wisnesky. JSC, 46(2):95-118, 2011. [doi]

Using constraint programming to verify DOPLER variability modelsRaúl Mazo, Paul Grünbacher, Wolfgang Heider, Rick Rabiser, Camille Salinesi, Daniel Diaz. vamos 2011: 97-103 [doi]

Verifying Functional Correctness of C Programs with VCCMichal Moskal. NFM 2011: 56-57 [doi]

SEAL: a logic programming framework for specifying and verifying access control modelsPrasad Naldurg, Raghavendra K. R.. SACMAT 2011: 83-92 [doi]

Verifying higher-order functional programs with pattern-matching algebraic data typesC.-H. Luke Ong, Steven James Ramsay. POPL 2011: 587-598 [doi]

Practical verification of high-level dataraces in transactional memory programsVasco Pessanha, Ricardo J. Dias, João Lourenço, Eitan Farchi, Diogo Sousa. ISSTA 2011: 26-34 [doi]

Automatically Refining Partial Specifications for Program VerificationShengchao Qin, Chenguang Luo, Wei-Ngan Chin, Guanhua He. fm 2011: 369-385 [doi]

Simulated verification of NC part programs from 2D imagesS. Srinivasa Rao, B. Satyanarayana, M. M. M. Sarcar. ijcim, 24(9):800-810, 2011. [doi]

Matching logic: a new program verification approach (NIER track)Grigore Rosu, Andrei Stefanescu. ICSE 2011: 868-871 [doi]

Automatic formal verification of MPI-based parallel programsStephen F. Siegel, Timothy K. Zirkel. ppopp 2011: 309-310 [doi]

Efficient Formal Verification of Bounds of Linear ProgramsAlexey Solovyev, Thomas C. Hales. mkm 2011: 123-132 [doi]

Formalisation and verification of programmable logic controllers timers in CoqHai Wan, Gang Chen, Xiaoyu Song, Ming Gu. iee, 5(1):32-42, 2011. [doi]

2010

OWASP Top 10 - 2010. The Ten Most Critical Web Application Security RisksTechnical Report 2010.

Testing First-Order Logic Axioms in Program VerificationKi Yung Ahn, Ewen Denney. tap 2010: 22-37 [doi]

Practical Aspects of Automated Deduction for Program VerificationWolfgang Ahrendt, Bernhard Beckert, Martin Giese, Philipp Rümmer. ki, 24(1):43-49, 2010. [doi]

Precise and Automated Contract-Based Reasoning for Verification and Certification of Information Flow Properties of Programs with ArraysTorben Amtoft, John Hatcliff, Edwin RodrÃguez. ESOP 2010: 43-63 [doi]

Multi-Prover Verification of Floating-Point ProgramsAli Ayad, Claude Marché. cade 2010: 127-141 [doi]

MERCURIO: An Interaction-oriented Framework for Designing, Verifying and Programming Multi-Agent SystemsMatteo Baldoni, Cristina Baroglio, Federico Bergenti, Antonio Boccalatte, Elisa Marengo, Maurizio Martelli, Viviana Mascardi, Luca Padovani, Viviana Patti, Alessandro Ricci, Gianfranco Rossi, Andrea Santi. woa 2010: [doi]

Formal Verification of Timed VHDL ProgramsAbdelrezzak Bara, Pirouz Bazargan-Sabet, Remy Chevallier, Dominique Ledu, Emmanuelle Encrenaz, Patricia Renault. fdl 2010: 80-85

Formal Modeling and Verification of Low-Level Software ProgramsBjörn Bartels, Sabine Glesner. qsic 2010: 200-207 [doi]

On Automated Program Construction and VerificationRudolf Berghammer, Georg Struth. mpc 2010: 22-41 [doi]

Using Constraints to Verify Properties of Rule ProgramsBruno Berstel, Michel Leconte. icst 2010: 349-354 [doi]

Program Verification in SPARK and ACSL: A Comparative Case StudyEduardo Brito, Jorge Sousa Pinto. Ada-Europe 2010: 97-110 [doi]

Path-Oriented Reachability Verification of a Class of Nonlinear Hybrid Automata Using Convex ProgrammingLei Bu, Jianhua Zhao, Xuandong Li. vmcai 2010: 78-94 [doi]

Program verification through characteristic formulaeArthur Charguéraud. ICFP 2010: 321-332 [doi]

Programmable Verifiers in Imperative ProgrammingYifeng Chen. utp 2010: 172-187 [doi]

Dynamic Verification of Hybrid ProgramsWei-Fan Chiang, Grzegorz Szubzda, Ganesh Gopalakrishnan, Rajeev Thakur. pvm 2010: 298-301 [doi]

Graph-based verification of static program constraintsSelim Ciraci, Pim van den Broek, Mehmet Aksit. SAC 2010: 2265-2272 [doi]

On the Verification of Very Expressive Temporal Properties of Non-terminating Golog ProgramsJens Claßen, Gerhard Lakemeyer. ecai 2010: 887-892 [doi]

Local Verification of Global Invariants in Concurrent ProgramsErnie Cohen, Michal Moskal, Wolfram Schulte, Stephan Tobies. cav 2010: 480-494 [doi]

CPBPV: a constraint-programming framework for bounded program verificationHélène Collavizza, Michel Rueher, Pascal Van Hentenryck. constraints, 15(2):238-264, 2010. [doi]

GamaSlicer: an online laboratory for program verification and analysisDaniela Carneiro da Cruz, Pedro Rangel Henriques, Jorge Sousa Pinto. LDTA 2010: 3 [doi]

Genetic Programming for Robust Text Independent Speaker VerificationPeter Day, Asoke K. Nandi. In Raymond Chiong, editor, Nature-Inspired Informatics for Intelligent Applications and Knowledge Discovery: Implications in Business, Science, and Engineering. pages 259-280, IGI Global, 2010. [doi]

Static Analysis, Abstract Interpretation and Verification in (Constraint Logic) ProgrammingGiorgio Delzanno, Roberto Giacobazzi, Francesco Ranzato. agp 2010: 136-158 [doi]

Modeling and Verifying Concurrent Programs with Finite Chu SpacesXutao Du, Chun-Xiao Xing, Li-Zhu Zhou. jcst, 25(6):1168-1183, 2010. [doi]

Program Specialization for Verifying Infinite State Systems: An Experimental EvaluationFabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Valerio Senni. LOPSTR 2011: 164-183 [doi]

Proceedings of the 4th ACM Workshop Programming Languages meets Program Verification, PLPV 2010, Madrid, Spain, January 19, 2010Cormac Flanagan, Jean-Christophe Filliâtre, editors, ACM, 2010.

Formal verification of concurrent programs with read-write locksMing Fu, Yu Zhang, Yong Li. fcsc, 4(1):65-77, 2010. [doi]

Probabilistic Verification Techniques and Probabilistic Program AnalysisAndreas Gaiser. dagstuhl 2010: 148 [doi]

Automata-based verification of programs with tree updatesPeter Habermehl, Radu Iosif, TomÃ¡s Vojnar. ACTA, 47(1):1-31, 2010. [doi]

Programming assistance based on contracts and modular verification in the automation domainDominik Hurnaus, Herbert Prähofer. SAC 2010: 2544-2551 [doi]

A Quick Tour of the VeriFast Program VerifierBart Jacobs, Jan Smans, Frank Piessens. aplas 2010: 304-311 [doi]

Challenge benchmarks for verification of real-time programsTomÃ¡s Kalibera, Pavel Parizek, Ghaith Haddad, Gary T. Leavens, Jan Vitek. plpv 2010: 57-62 [doi]

Higher-order multi-parameter tree transducers and recursion schemes for program verificationNaoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno. POPL 2010: 495-508 [doi]

Verifying event-driven programs using ramified frame propertiesNeel R. Krishnaswami, Lars Birkedal, Jonathan Aldrich. tldi 2010: 63-76 [doi]

Verification and falsification of programs with loops using predicate abstractionDaniel Kroening, Georg Weissenbacher. fac, 22(2):105-128, 2010. [doi]

Certificate Translation for the Verification of Concurrent ProgramsCésar Kunz. tgc 2010: 237-252 [doi]

Multilevel Dual-Channel NAND Flash Memories with High Read and Program Verifying Speeds Utilizing Asymmetrically-Doped Channel RegionsJoung Woo Lee, Joo Hyung You, Sang Hyun Jang, Kae-Dal Kwack, Tae-Whan Kim. ieicet, 93-C(5):654-657, 2010. [doi]

Learning to do program verificationK. Rustan M. Leino. CACM, 53(6):106, 2010. [doi]

Verifying Concurrent Programs with ChaliceK. Rustan M. Leino. vmcai 2010: 2 [doi]

Dafny: An Automatic Program Verifier for Functional CorrectnessK. Rustan M. Leino. lpar 2010: 348-370 [doi]

A symbolic verifier for CUDA programsGuodong Li, Ganesh Gopalakrishnan, Robert M. Kirby, Dan Quinlan. ppopp 2010: 357-358 [doi]

API Conformance Verification for Java ProgramsXin Li, H. James Hoover, Piotr Rudnicki. icfem 2010: 188-203 [doi]

Complete Verification of Weakly Programmable IPs against Their Operational ISA ModelSacha Loitz, Markus Wedler, Dominik Stoffel, Christian Brehm, Norbert Wehn, Wolfgang Kunz. fdl 2010: 29-36

Verification of Structural Pattern Conformance Using Logic ProgrammingLunjin Lu, Dae-Kyoo Kim, Yuanlin Zhu, Sangsig Kim. jucs, 16(17):2455-2474, 2010. [doi]

Verifying pointer safety for programs with unknown callsChenguang Luo, Florin Craciun, Shengchao Qin, Guanhua He, Wei-Ngan Chin. JSC, 45(11):1163-1183, 2010. [doi]

Lazy Annotation for Program Testing and VerificationKenneth L. McMillan. cav 2010: 104-118 [doi]

Abductive Logic Programming as an Effective Technology for the Static Verification of Declarative Business ProcessesMarco Montali, Paolo Torroni, Federico Chesani, Paola Mello, Marco Alberti, Evelina Lamma. FUIN, 102(3-4):325-361, 2010. [doi]

Structuring the verification of heap-manipulating programsAleksandar Nanevski, Viktor Vafeiadis, Josh Berdine. POPL 2010: 261-274 [doi]

Verifying Heap-Manipulating Programs with Unknown Procedure CallsShengchao Qin, Chenguang Luo, Guanhua He, Florin Craciun, Wei-Ngan Chin. icfem 2010: 171-187 [doi]

Correctness Verification of Generalized Algebraic Deadlock Avoidance Policies Through Mathematical ProgrammingSpyros A. Reveliotis, Elzbieta Roszkowska, Jin-Young Choi. tase, 7(2):240-248, 2010. [doi]

Constraint Solving for Program Verification: Theory and Practice by ExampleAndrey Rybalchenko. csl 2010: 51 [doi]

Constraint Solving for Program Verification: Theory and Practice by ExampleAndrey Rybalchenko. cav 2010: 57-71 [doi]

Automatic verification of Java programs with dynamic framesJan Smans, Bart Jacobs, Frank Piessens, Wolfram Schulte. fac, 22(3-4):423-457, 2010. [doi]

Relationship between the Verification Based Model and the Functional Dependences Model Using Program SpecificationSafeeullah Soomro, Abdul Baqi. icic 2010: 535-542 [doi]

From program verification to program synthesisSaurabh Srivastava, Sumit Gulwani, Jeffrey S. Foster. POPL 2010: 313-326 [doi]

Verifying parallel programs with dynamic communication structuresTayssir Touili, Mohamed Faouzi Atig. TCS, 411(38-39):3460-3468, 2010. [doi]

Automatic Verification of Determinism for Structured Parallel ProgramsMartin T. Vechev, Eran Yahav, Raghavan Raman, Vivek Sarkar. SAS 2010: 455-471 [doi]

Formal polytypic programs and proofsWendy Verbruggen, Edsko de Vries, Arthur Hughes. JFP, 20(3-4):213-269, 2010. [doi]

Scalable verification of MPI programsAnh Vo, Ganesh Gopalakrishnan. ipps 2010: 1-4 [doi]

A Scalable and Distributed Dynamic Formal Verifier for MPI ProgramsAnh Vo, Sriram Aananthakrishnan, Ganesh Gopalakrishnan, Bronis R. de Supinski, Martin Schulz, Greg Bronevetsky. sc 2010: 1-10 [doi]

Automated Program Verification Using Generation of InvariantsJianying Xing, Mengjun Li, Zhoujun Li. qsic 2010: 300-305 [doi]

Verifying safety properties of concurrent heap-manipulating programsEran Yahav, Mooly Sagiv. TOPLAS, 32(5), 2010. [doi]

Trace-Driven Verification of Multithreaded ProgramsZijiang Yang, Karem Sakallah. icfem 2010: 404-419 [doi]

Axiomatic Temporal Logic Programs VerificationXiaoxiao Yang, Zhenhua Duan. tase 2010: 87-94 [doi]

Recent advances in program verification through computer algebraLu Yang, Chaochen Zhou, Naijun Zhan, Bican Xia. fcsc, 4(1):1-16, 2010. [doi]

CPN Tools Application in Verification of Parallel ProgramsLulu Zhu, Weiqin Tong, Bin Cheng. icica 2011: 137-143 [doi]

PreviousNext