Sofia Vieira Pinto; Álvaro F. Silva; João Pascoal Faria; Alexandra Mendes
Ringkasan
DSpec2Test secara otomatis menurunkan tes dari spesifikasi Dafny menggunakan partisi kelas ekuivalen DNF dan Boundary Value Analysis opsional, mencapai tingkat pembunuhan mutasi 93,9% dibandingkan 82,4% untuk mode Block Dafny.
Metode
DSpec2Test beroperasi sebagai pembuat tes blackbox: ia mengambil spesifikasi Dafny (prasyarat, pascasyarat, dan invarian) dan mengabaikan badan implementasi. Algoritma inti mempar…
Hasil
Evaluasi membandingkan DSpec2Test dengan mode Block berbasis implementasi Dafny yang ada pada dataset 131 mutan yang dihasilkan dari program DafnyBench menggunakan MutDafny. Metrik utamanya adalah ti…
ProofPulse adalah alat untuk Dafny yang mendiagnosis kualitas spesifikasi menggunakan model cakupan pembuktian tiga nilai, yang membedakan maksud spesifikasi, pemeriksaan tambahan, dan elemen yang tidak relevan. Dievaluasi pada 252 program…
Metode
ProofPulse memperkenalkan model cakupan pembuktian tiga nilai untuk mengklasifikasikan elemen spesifikasi berdasarkan perannya dalam kewajiban pembuktian. Model ini menganalisis d…
Hasil
ProofPulse dievaluasi terhadap oracle 252 program dari benchmark dafny-synthesis. Hasilnya menunjukkan bahwa ProofPulse memberikan sinyal presisi tinggi untuk kelemahan spesifikasi, khususnya prasyar…
Penekanan positif palsu dalam aturan deteksi menumpuk sebagai ratchet satu arah: pengecualian ditambahkan jauh lebih sering daripada ditarik, bertahan bertahun-tahun, dan tidak ditriase berdasarkan konsekuensi. Penulis mengukurnya secara s…
Metode
Studi ini menganalisis korpus SigmaHQ selama sembilan tahun, mencakup 8.234 revisi. Penekanan dideteksi secara semantik, bukan struktural. Secara formal, misalkan revisi aturan di…
Hasil
Hasil empirisnya mencolok. Di seluruh korpus, pengecualian ditambahkan 1.642 kali dan ditarik 304 kali, menghasilkan rasio keseluruhan 5,4 banding 1. Pada tingkat aturan individual, rasio naik menjad…
AutoSciRub menginduksi rubrik yang dapat dieksekusi dan spesifik tugas sebelum eksekusi penelitian, lalu menggunakannya untuk memandu eksperimen, verifikasi tingkat kriteria, dan revisi iteratif. Pendekatan ini meningkatkan performa pada R…
Metode
AutoSciRub beroperasi dalam tiga tahap utama: 1. **Induksi Rubrik**: Kerangka kerja ini menguraikan instruksi yang kurang spesifik menjadi tujuan ilmiah atomik, mendasarkannya pad…
Hasil
Penulis mengevaluasi AutoSciRub pada dua tolok ukur: **ResearchClawBench** dan **AstaBench E2E Discovery**. - Pada ResearchClawBench, AutoSciRub secara konsisten meningkatkan semua konfigurasi yang d…
Gopi Krishnan Rajbahadur; Amir M. Ebrahimi; Boyuan Chen; Ahmed E. Hassan
Ringkasan
Post-training industri mewarisi checkpoint yang sudah diterapkan dan harus menghasilkan perbaikan yang ditargetkan di bawah anggaran komputasi dan campuran yang tetap tanpa menurunkan performa lainnya. Penulis berpendapat artefak yang dipe…
Metode
Studi ini adalah studi kasus industri tentang upaya peningkatan pembuatan kode. Unit intervensinya adalah **mixture patch terbatas** yang diterapkan pada checkpoint yang diwarisi,…
Hasil
Patch yang direkayasa yield menghasilkan keuntungan terukur dan signifikan secara statistik dari satu checkpoint tetap per kondisi, di seluruh 16 evaluasi stokastik setiap benchmark. | Benchmark | Me…
Yisen Xi mengusulkan protokol audit forensik empat tahap yang merekonstruksi konfigurasi saat peluncuran, mengambil sidik jari katalog platform, menguji identitas tokenizer melalui diferensial lintas panjang, dan mengonfirmasi dengan probe…
Metode
## Protokol Audit Forensik Empat Tahap ### Tahap 0 — Rekonstruksi Konfigurasi Saat Peluncuran Tahap 0 merekonstruksi konfigurasi saat peluncuran dari **snapshot platform yang diar…
Hasil
## Konsistensi Deklarasi dan Validasi Prospektif ### Hasil Himpunan Uji (10 Rilis Beridentitas Diketahui) | Hasil | Jumlah | |---|---| | Persis | 7 | | Perbedaan presisi | 2 | | Parsial | 1 | | Berla…
Diff yang ditulis LLM dan penulisan ulang berkas penuh tidak aman untuk remediasi GitOps tanpa pengawasan, dengan patching toleran secara diam-diam salah menerapkan 14-20% suntingan. Pipeline deterministik yang menerapkan maksud perubahan …
Metode
Evaluasi membandingkan dua strategi generasi teks yang digerakkan LLM dengan pipeline deterministik yang diusulkan. Pertama, diff terpadu diuji dengan patching ketat dan patching …
Hasil
Diff terpadu tidak aman untuk otomasi tanpa pengawasan. Di bawah patching ketat, hampir tidak ada yang diterapkan, tetapi ini adalah artefak dari kekakuan. Alat toleran seperti GNU patch menerapkan 9…
Daniel Bund; Julian Erhard; Michael Petter; Michael Schwarz
Ringkasan
Makalah ini memperluas kerangka deteksi data race statis untuk menangani thread barrier dan pthread_once, lalu menginstansiasinya dengan abstraksi lockset yang dipegang oleh thread leluhur. Serangkaian litmus test mengungkap bahwa perkakas…
Metode
Penulis membangun di atas kerangka digest, yang melacak abstraksi riwayat eksekusi thread untuk meningkatkan presisi deteksi race. Mereka memperkenalkan dua perluasan utama: 1. **…
Hasil
Evaluasi berfokus pada dua aspek: (1) kemampuan kerangka digest yang diperluas untuk menangani barrier dan `pthread_once`, dan (2) perbandingan dengan detektor race statis mutakhir yang ada. Penulis …
Digest ini merangkum wawancara dengan Ciera Jaspan dan Collin Green dari tim Developer Intelligence Google, membahas bagaimana empirical software engineering (ESE) diterapkan di industri, termasuk metode penelitian, pengambilan keputusan, …
Metode
Digest ini didasarkan pada wawancara semi-terstruktur dengan dua praktisi industri. Format wawancara memungkinkan eksplorasi mendalam tentang praktik ESE di Google. Penulis menyun…
Hasil
Wawancara mengungkap bahwa tim Developer Intelligence Google menerapkan berbagai metode ESE untuk mempelajari produktivitas developer dan proses rekayasa perangkat lunak. Temuan utama meliputi: - **M…
Jessica Diaz; Joaquin Gayoso; Andrea Cimminio; Jorge Perez
Ringkasan
Makalah ini menetapkan Spec-Driven Development (SDD) sebagai disiplin pemungkin untuk Agentic Software Engineering pada skala tim, memperkenalkan model sosio-teknis, karakterisasi harness ganda, dan lima pola interaksi manusia-agen. Makala…
Metode
Studi ini melakukan **analisis konseptual** yang terutama bersumber dari gray literature—makalah visi dan peta jalan ASE, laporan praktisi, ceramah, dan perkakas—karena bukti peer…
Hasil
Makalah ini menyajikan tiga hasil utama: **(i) Model sosio-teknis SDD.** Spesifikasi dinaikkan dari artefak dokumentasi menjadi *kontrak yang dapat dieksekusi* yang mengikat niat manusia pada perilak…
