Model Checking Visual Specification of Requirements. - Ulka Shrotri; Purandar Bhaduri; R. Venkatesh 001 (SEFM, 2003)

Visual specification and analysis of use cases. - Deepali Kholkar; G. Murali Krishna; Ulka Shrotri; R. Venkatesh 001 (SOFTVIS, 2005)

Methods and Tools for Formal Software Engineering. - Zhiming Liu 001; R. Venkatesh 001 (VSTTE, 2005)

Automatic Test Data Generation for C Programs. - Prasad Bokil; Priyanka Darke; Ulka Shrotri; R. Venkatesh 001 (SSIRI, 2009)

Proving unreachability using bounded model checking. - Ulka Shrotri; R. Venkatesh 001; Ravindra Metta (ISEC, 2010)

Feature based Structuring and Composing of SDLC Artifacts. - Nishigandha Hirve; Tukaram Muske; Ulka Shrotri; R. Venkatesh 001 (SEKE, 2010)

Masking Boundary Value Coverage: Effectiveness and Efficiency. - P. Vijay Suman; Tukaram Muske; Prasad Bokil; Ulka Shrotri; R. Venkatesh 001 (TAIC PART, 2010)

Precise Analysis of Large Industry Code. - Priyanka Darke; Mayur Khanzode; Arun Nair; Ulka Shrotri; R. Venkatesh 001 (APSEC, 2012)

Effectiveness of Random Testing of Embedded Systems. - Padmanabhan Krishnan; R. Venkatesh 001; Prasad Bokil; Tukaram Muske; P. Vijay Suman (HICSS, 2012)

Trace based reachability verification for statecharts. - Kumar Madhukar; Ravindra Metta; Ulka Shrotri; R. Venkatesh 001 (FormaliSE@ICSE, 2013)

Reachability Verification of Rhapsody Statecharts. - Kumar Madhukar; Ravindra Metta; Priyanka Singh; R. Venkatesh 001 (ICST Workshops, 2013)

Scaling Model Checking for Test Generation Using Dynamic Inference. - Anand Yeolekar; Divyesh Unadkat; Vivek Agarwal; Shrawan Kumar 001; R. Venkatesh 001 (ICST, 2013)

EDT: A specification notation for reactive systems. - R. Venkatesh 001; Ulka Shrotri; G. Murali Krishna; Supriya Agrawal (DATE, 2014)

Over-approximating loops to prove properties using bounded model checking. - Priyanka Darke; Bharti Chimdyalwar; R. Venkatesh 001; Ulka Shrotri; Ravindra Metta (DATE, 2015)

Cost-effective Functional Testing of Reactive Software. - R. Venkatesh 001; Ulka Shrotri; Amey Zare; Supriya Agrawal (ENASE, 2015)

On Generating Test Cases from EDT Specifications. - R. Venkatesh 001; Ulka Shrotri; Amey Zare; Supriya Agrawal (ENASE (Selected Papers), 2015)

Achieving Effective Test Suites for Reactive Systems using Specification Mining and Test Suite Reduction Techniques. - Prasad Bokil; Padmanabhan Krishnan; R. Venkatesh 001 (ACM SIGSOFT Softw. Eng. Notes, 2015)

TIC: a scalable model checking based approach to WCET estimation. - Ravindra Metta; Martin Becker 001; Prasad Bokil; Samarjit Chakraborty; R. Venkatesh 001 (LCTES, 2016)

Scaling Bounded Model Checking by Transforming Programs with Arrays. - Anushri Jana; Uday P. Khedker; Advaita Datar; R. Venkatesh 001; Niyas C (LOPSTR, 2016)

Efficient Safety Proofs for Industry-Scale Code Using Abstractions and Bounded Model Checking. - Priyanka Darke; Bharti Chimdyalwar; Avriti Chauhan; R. Venkatesh 001 (ICST, 2017)

VeriAbs: Verification by Abstraction (Competition Contribution). - Bharti Chimdyalwar; Priyanka Darke; Avriti Chauhan; Punit Shah; Shrawan Kumar 001; R. Venkatesh 001 (TACAS (2), 2017)

Sequentialization Using Timestamps. - Anand Yeolekar; Kumar Madhukar; Dipali Bhutada; R. Venkatesh 001 (TAMC, 2017)

Generalizing specific-instance interpolation proofs with SyGuS. - Muqsit Azeem; Kumar Madhukar; R. Venkatesh 001 (ICSE (NIER), 2018)

Refining Task Specifications using Model Checking. - Anand Yeolekar; Ravindra Metta; R. Venkatesh 001; Samarjit Chakraborty (RTCSA, 2018)

Efficiently Learning Safety Proofs from Appearance as well as Behaviours. - Sumanth Prabhu 001; Kumar Madhukar; R. Venkatesh 001 (SAS, 2018)

VeriAbs: Verification by Abstraction and Test Generation - (Competition Contribution). - Priyanka Darke; Sumanth Prabhu 001; Bharti Chimdyalwar; Avriti Chauhan; Shrawan Kumar 001; Animesh Basak Chowdhury; R. Venkatesh 001; Advaita Datar; Raveendra Kumar Medicherla (TACAS (2), 2018)

Property Checking Array Programs Using Loop Shrinking. - Shrawan Kumar 001; Amitabha Sanyal; R. Venkatesh 001; Punit Shah (TACAS (1), 2018)

Scalable and Precise Estimation and Debugging of the Worst-Case Execution Time for Analysis-Friendly Processors. - Martin Becker 001; Ravindra Metta; R. Venkatesh 001; Samarjit Chakraborty (CoRR, 2018)

VeriAbs : Verification by Abstraction and Test Generation. - Mohammad Afzal; Asia A; Avriti Chauhan; Bharti Chimdyalwar; Priyanka Darke; Advaita Datar; Shrawan Kumar 001; R. Venkatesh 001 (ASE, 2019)

Imprecision in WCET estimates due to library calls and how to reduce it (WIP paper). - Martin Becker 001; Samarjit Chakraborty; Ravindra Metta; R. Venkatesh 001 (LCTES, 2019)

VeriFuzz: Program Aware Fuzzing - (Competition Contribution). - Animesh Basak Chowdhury; Raveendra Kumar Medicherla; R. Venkatesh 001 (TACAS (3), 2019)

Scalable and precise estimation and debugging of the worst-case execution time for analysis-friendly processors: a comeback of model checking. - Martin Becker 001; Ravindra Metta; R. Venkatesh 001; Samarjit Chakraborty (Int. J. Softw. Tools Technol. Transf., 2019)

Using hypersafety verification for proving correctness of programming assignments. - Jude K. Anil; Sumanth Prabhu S; Kumar Madhukar; R. Venkatesh 001 (ICSE (NIER), 2020)

Scaling Test Case Generation For Expressive Decision Tables. - Supriya Agrawal; R. Venkatesh 001; Ulka Shrotri; Amey Zare; Sagar Verma (ICST, 2020)

VeriAbs : Verification by Abstraction and Test Generation (Competition Contribution). - Mohammad Afzal; Supratik Chakraborty; Avriti Chauhan; Bharti Chimdyalwar; Priyanka Darke; Ashutosh Gupta 001; Shrawan Kumar 001; Charles Babu M; Divyesh Unadkat; R. Venkatesh 001 (TACAS (2), 2020)

EImprove - Optimizing Energy and Comfort in Buildings based on Formal Semantics and Reinforcement Learning. - Sagar Verma; Supriya Agrawal; R. Venkatesh 001; Ulka Shrotri; Srinarayana Nagarathinam; Rajesh Jayaprakash; Aabriti Dutta (DAC, 2021)

Fast Change-Based Alarm Reporting for Evolving Software Systems. - Anushri Jana; Ankita Khadsare; Bharti Chimdyalwar; Shrawan Kumar 001; Vaidehi Ghime; R. Venkatesh 001 (ISSRE, 2021)

VeriAbs: A Tool for Scalable Verification by Abstraction (Competition Contribution). - Priyanka Darke; Sakshi Agrawal; R. Venkatesh 001 (TACAS (2), 2021)

Direct Construction of Program Alignment Automata for Equivalence Checking. - Manish Goyal 002; Muqsit Azeem; Kumar Madhukar; R. Venkatesh 001 (CoRR, 2021)

Automated Validation of Insurance Applications against Calculation Specifications. - Advaita Datar; Amey Zare; Asia A; R. Venkatesh 001; Shrawan Kumar 001; Ulka Shrotri (ISSRE Workshops, 2022)

Fast Analysis of Evolving Software Systems. - Anushri Jana; Bharti Chimdyalwar; Shrawan Kumar 001; R. Venkatesh 001 (ISSRE Workshops, 2022)

Impactful research and tooling for program correctness. - Priyanka Darke; Ravindra Metta; Raveendra Kumar Medicherla; R. Venkatesh 001 (Commun. ACM, 2022)

Towards Synthesis of Code for Calculations Using Their Specifications. - Advaita Datar; Amey Zare; R. Venkatesh 001; Asia A (ENASE, 2023)

VeriAbsL: Scalable Verification by Abstraction and Strategy Prediction (Competition Contribution). - Priyanka Darke; Bharti Chimdyalwar; Sakshi Agrawal; Shrawan Kumar 001; R. Venkatesh 001; Supratik Chakraborty (TACAS (2), 2023)

The VeriAbs Tool Suite for Code Verification. - Priyanka Darke; Bharti Chimdyalwar; R. Venkatesh 001; Supratik Chakraborty (ATVA, 2024)

Detecting Covert Channels in Cloud Access Control Policies Using Large Language Models. - Hrishikesh Karmarkar; Vaibhavi Joshi; R. Venkatesh 001 (CSR, 2024)

Learning Strategies Using Boolean Program Metrics to Verify Industrial Code. - Priyanka Darke; Bharti Chimdyalwar; Manoj Alladawar; Sahil Sulakhe; R. Venkatesh 001; Supratik Chakraborty (ICSME, 2024)

PROTON: PRObes for Termination Or Not (Competition Contribution). - Ravindra Metta; Hrishikesh Karmarkar; Kumar Madhukar; R. Venkatesh 001; Supratik Chakraborty (TACAS (3), 2024)

Weakest Precondition Inference for Non-Deterministic Linear Array Programs. - Sumanth Prabhu 001; Deepak D'Souza; Supratik Chakraborty; R. Venkatesh 001; Grigory Fedyukovich (TACAS (2), 2024)

A shallow dive into the depths of non-termination checking for C programs. - Ravindra Metta; Hrishikesh Karmarkar; Kumar Madhukar; R. Venkatesh 001; Supratik Chakraborty; Samarjit Chakraborty (CoRR, 2024)

Deterministic Suffix-reading Automata. - R. Keerthan; B. Srivathsan; R. Venkatesh 001; Sagar Verma (GandALF, 2024)

Repairing Control Safety Violations via Scheduler Patch Synthesis. - Anand Yeolekar; Supratik Chakraborty; R. Venkatesh 001; Samarjit Chakraborty (ICCPS, 2025)